cv

Dale Miller
Curriculum Vitae

INRIA Saclay - Île-de-France & Laboratoire d’Informatique, LIX
École polytechnique
91128 PALAISEAU Cedex, FRANCE
dale.miller @ inria.fr
http://www.lix.polytechnique.fr/Labo/Dale.Miller/
Phone: (+33) 01 69 33 41 34, Fax: (+33) 01 69 33 30 14

Employment

September 2002 – Present: Directeur de Recherche, INRIA Saclay.
September 2002 – December 2006: Professor, Ècole polytechnique.
September 1997 – July 2001: Professor and Head. August 2001 – August 2002, Professor. Department of Computer Science and Engineering, The Pennsylvania State University.
1989 – 1997: Associate Professor with tenure, University of Pennsylvania
1983 – 1989: Assistant Professor, University of Pennsylvania
1978 – 1983: Research Assistant, Carnegie Mellon University
Summers 1977, 78: Mathematician, AI Lab, National Bureau of Standards (now NIST)

Supported Visiting Positions

February 2002: Guest professor, University Aix-Marseille 2 at the IML, Luminy.
23 January – 22 February 1997: Visiting Professor at the University of Sienna.
1 September – 31 October 1996: Visiting Professor at the University of Genoa.
July 1994: Visiting Professor at the Universities of Pisa and Genoa.
July 1991 – September 1991: SERC Visiting Fellow, University of Glasgow.
September 1990 – June 1991: Visiting Research Scientist, LFCS, University of Edinburgh.

Education

Ph.D. Mathematics, Carnegie Mellon University, December 1983. Supervised by Peter Andrews.
B.S. Mathematics, Lebanon Valley College, May 1978.

Major Research Interests

Computational logic, proof theory, linear logic, unification, proof search, game semantics.
Declarative programming languages, particularly the logic and concurrency paradigms: their theory, design, and implementation.
The specification of and reasoning about the operational semantics for programming languages.

Personal Information

Married to Catuscia Palamidessi, an Italian citizen.
Two children: Nadia (1999) and Alexis (2003).
USA citizen. Titre de sejour, France.

Invited Speaker at Conferences and Workshops

ANR-DFG Hypothese Workshop titled Different Aspects of Proof Theory, ENS Paris, 2 or 3 May 2012.
Journees nationales du GDR-IM, 25-26 January 2012, University of Paris 7.
LMPS 2011: 14th International Congress of Logic, Methodology and Philosophy of Science, Nancy, France, 19-26 July 2011 (Section C1: Logic, Mathematics and Computer Science).
APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, Shanghai Jiao Tong University, China, November 29 - December 1, 2010.
FICS 2010: 7th Workshop on Fixed Points in Computer Science, Brno, Czech Republic, 21-22 August 2010.
MLPA: 2nd Workshop on Module Systems and Libraries for Proof Assistants, a FLoC 2010 workshop associated with IJCAR and ITP, 15 July 2010.
Colloquium on Games, Dialogue and Interaction, Université Paris 8, 28-29 September 2009.
LAM 2009: Logics for Agents and Mobility. A workshop associated to LICS09. 9-10 August 2009.
Journées du projet PEPS-Relations, University of Paris XIII, 15 - 16 December 2008.
APS: 4th International Workshop on Analytic Proof Systems, part of LPAR 2008, Doha, Qatar, 22 November 2008.
SOS 2008: Structural Operational Semantics, an affiliated workshop of ICALP 2008, Reykjavik, Iceland, 6 July 2008.
WFLP 2008: 17th International Workshop on Functional and (Constraint) Logic Programming, Siena, 3-4 July 2008.
LFMTP 2008: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (affiliated with LICS08), Pittsburgh, 23 June 2008.
Dimostrazioni, Polaritá e Cognizione, Facoltà di Lettere e Filosofia, Università di Roma Tre, 18 April 2008.
Collegium Logicum 2007: Proofs and Structures, 24-25 October 2007, Vienna, Austria.
IJCAR 2006: Joint Conference on Automated Reasoning (part of FLoC 2006). Seattle, 16-21 August 2006.
Geometria della Logica, Facoltà di Lettere e Filosofia, Università di Roma Tre, 28-29 April 2006.
Algebraic Process Calculus: The first 25 years and beyond, Bertinoro, Italy, 5 August 2005.
Structure and Deduction 2005: an ICALP workshop, Lisbon, 16-17 July 2005.
2nd Taiwanese-French Conference in Information Technologies, Tainan, Taiwan, 23-25 March 2005.
CSL 2004: 13th Annual Conference of the European Association for Computer Science Logic, Karkonoski National Park, Poland, 20-23 September 2004.
TPHOLs 2003: International Conference on Theorem Proving in Higher Order Logics, 9-12 September 2003, Rome, Italy.
Wollic 2003: 10th Workshop on Logic, Language, Information and Computation, 29 July - 1 August 2003, Ouro Preto, Minas Gerais, Brazil.
Workshop on Process Algebra, Bertinoro, Italy, 23 July 2003.
UNIF 2003: 17th International Workshop on Unification, 8-9 June 2003, Valencia, Spain.
FSTTCS02: 22nd Foundations of Software Technology and Theoretical Computer Science, 12-14 December 2002, Indian Institute of Technology, Kanpur, India.
AMAST02: 9th International Conference on Algebraic Methodology And Software Technology, September 9-13, 2002, St. Gilles les Bains, Reunion Island, France.
TABLEAUX 2002: Automated Reasoning with Analytic Tableaux and Related Methods. Copenhagen, Denmark, July 30 - August 1, 2002.
Second International Workshop on Foundations for Secure/Survivable Systems and Networks, 26 - 27 October 2001, Tokyo Institute of Technology, Tokyo, Japan.
RTA 2000: 11th International Conference on Rewriting Techniques and Applications, 10-12 July 2000, University of East Anglia, Norwich, U.K.
European Meeting of the Association for Symbolic Logic, Utrecht, 1-6 August 1999.
TYPES’96: Workshop on Types, Aussois, France, 16-19 December 1996.
Conference on Logical Aspects of Computational Linguistics, Nancy, 23-25 September 1996.
Conference on Logics and Models of Computation, Marseille, 16 – 20 September 1996.
Linear Logic ’96, Tokyo, Japan, 29 March – 2 April 1996.
Second New Zealand Formal Program Development Colloquium, Massey, 14 - 15 February 1996.
Computing: The Australian Theory Seminar (CATS), Melbourne, 29 – 30 January 1996.
The Fourth Compulog meeting, Vietri, Italy, 15 September 1995.
GULP-PRODE’95: Italian-Spanish Joint Conference on Declarative Programming, Vietri, Italy, 11 – 14 September 1995.
Joint meeting of Algebraic and Logic Programming (ALP) and Programming Languages Implementation and Logic Programming (PLILP), Madrid, September 1994.
Fourth North American Jumelage meeting, SRI International, Menlo Park, CA, 13 – 17 October 1993.
Second Compulog-Network Subgroup Meeting on Programming Languages, Pisa, 6 – 7 May 1993.
MFPS’93: Ninth Conference on the Mathematical Foundations of Programming Semantics, New Orleans, LA, 7 – 10 April 1993.
Fourth Intern. Workshop on Extensions of Logic Programming, St. Andrews, Scotland, March 1993.
Workshop on Logic and Change during German AI Conference, Bonn, Germany, 18 – 19 Sept 1991.
Second Russian Conference on Logic Programming, St. Petersburg, 11 – 15 September 1991.
Logical Framework BRA ESPRIT Workshop, Edinburgh, 20 – 23 May 1991.
Esprit project on Computational Logic, University of Tübingen, Germany, 24 – 26 September 1990.
Esprit project on Logical Foundations, Nice, France, 7 – 12 May 1990.
Workshop on Extensions to Logic Programming, Tübingen, Germany, 8 – 9 December 1989.
Banff meeting on “Higher-Orders”, Canada, 23 – 28 September 1989.
Workshop on Proof, Cambridge University, England, 11 – 14 July 1988.
Workshop on Meta Language and Tools for Mechanizing Formal Deductive Theories, Carnegie Mellon University, 13 – 14 November 1987.
Sym. on Mathematical Foundations for Computer Science, IBM Japan, Oiso, Japan, 28 – 31 May 1985.
Alfred Tarski Memorial Conference on Logic, Truth and Type-Theory, Ohio State Univ, 8 April 1984.

Invited Tutorials and Advanced Courses

Graduate level course on “Proof theory with applications to computation and deduction,” Dipartimento di Informatica, Università di Pisa, 19-30 September 2011.
PLS8: 8th Panhellenic Logic Symposium, Ioannina, Greece, July 4-8, 2011. Three hour tutorial.
ISCL: International School on Computational Logic, Bertinoro, 10-15 April 2011. Six hours of lectures.
Graduate level course on “Proof search and Computation.” Dipartimento di Scienze dell’Informazione, Universitá degli studi di Milano, 15-26 March 2010.
Graduate level course on “Proof systems for linear, intuitionistic, and classical logic.” Dipartimento di Informatica, Universitá Ca’ Foscari di Venezia, 15-24 April 2009.
Wollic 2003: 10th Workshop on Logic, Language, Information and Computation, 29 July - 1 August 2003, Ouro Preto, Minas Gerais, Brazil.
Summer School on the Proofs-as-Programs Paradigm, Eugene, Oregon, June 24 - July 5, 2002. Sponsored by NSF, ACM SIGPLAN, and INRIA.
Workshop on Proof Theory and Computation, Dresden University of Technology, 3-14 June 2002.
International School on Computational Logic (ISCL), Acquafredda di Maratea (Basilicata, Italy), September 4-9, 2000. Sponsored by Association for Logic Programming (ALP), the European COMPULOG net and by GULP.
Eleventh European Summer School in Logic, Language and Information (ESSLLI-99), August 1999, Utrecht. Co-taught an introductory course of 7.5 hours with G. Nadathur.
International Summer School on the Logic of Computation, Marktoberdorf, an Advanced Study Institute of the NATO Science Committee and the Technische Universität München, Germany, 29 July – 10 August 1997.
Twenty hour course for PhD students at the University of Siena, Italy, 27 January – 11 Feburary 1997.
One week course for PhD students at the University of Padova, Italy, 15 —19 July 1996. Ten hours of lectures.
International Summer School on the Logic of Computation, Marktoberdorf, an Advanced Study Institute of the NATO Science Committee and the Technische Universität München, Germany, 25 July – 6 August 1995. Five hours of lectures. Lectures published by the NATO Press.
Two week course for PhD students at the University of Pisa, 30 May – 10 June 1994. Twenty hours.
Fourth International School for Computer Science Researchers, Acireale, Sicily, 22 June - 4 July 1992. Eight hours of lectures.
Second International School of Philosophy of Science, sponsored by the International Centre for Theoretical Physics, Trieste, Italy, 27 October – 10 November 1991. Five hours of lectures.
Third European Summer School in Language, Logic, and Information, Saarbrücken, 12 – 23 August 1991. Five hours of lectures.
International Conference on Logic Programming, July 1991. Three hours of tutorial.
ARO/ONR sponsored meeting on Formal Methods in Software Engineering, Ft. Monroe, 13 – 15 May 1991. Five hours of lectures.
ALP meeting (UK Chapter), Edinburgh, 10 – 12 April 1991. Three hours of tutorial.
International Conference on Automated Deduction, Kaiserslautern, Germany, July 1990. Three hours tutorial on jointly with Amy Felty, Elsa Gunter, and Frank Pfenning.
ICLP90: International Conference on Logic Programming, July 1990. 90 minutes tutorial.
Alghero, Sardinia, Italy, Advanced School on Foundations of Logic Programming, 17 – 23 September 1988. Six hours of tutorial.
MCC, Parallel Processing Group, Austin Texas, 30 June – 3 July 1986. Twenty hours of lectures.
Courses in Lisp and Prolog programming for the Army Research Office: March 1985, June 1985, January 1986, and June 1988.

Colloquia and Seminar Talks

2011: POP Seminar, Carnegie Mellon University, 17 October • School of Computer Science, Colloquium Series, McGill University, 14 October • Workshop on Proof Theory, Paris, 16 June 2011 • Chalmers University of Technology, Göteborg, Sweden, 23-24 May • Technical University of Vienna, 12 January.
2010: University of Minnesota, 10 November • University of Bath, 15 September • INRIA-Loria, Nancy, 12 March • LRI, University of Paris South, 8 October.
2008: Laboratoire "Preuves, programmes, systémes" (PPS), 13 Nov • Workshop on Proof-search in Type Theories, LIX, 5 June.
2007: ICMS Workshop on Mathematical Theories of Abstraction, Substitution and Naming in Computer Science, Edinburgh, UK, 25-29 May.
2006: LIX, Ecole Polytechnique, 15 June • Laboratoire "Preuves, programmes, systémes" (PPS), 1 December.
2005: Universidad Complutense Madrid, 29 Nov • University of Pisa, Italy, 22 July • WIPS 2005: Workshop on Implementations of Proof Search, University of Minnesota, 1 July • University of Minnesota, 19 April • Academia Sinica, Taiwan, 28 March • 2nd Taiwanese-French Conference in Information Technologies, Tainan, Taiwan, 23-25 March.
2004: INRIA-Loria, Nancy, 7 December. • University of Pisa, Italy, 5 July. • PPS Paris VII, 24 June • ACI Workshop on “Théorie des preuves des types inductifs et coinductifs”, 17 June • ACI Workshop on “Modèles pour la concurrence et la mobilité”, 26 May • LRI, CNRS-Université de Paris Sud, 30 January.
2003: Groupe de travail "Sémantique", PPS Paris VII, 2 December • Workshop PCRI-CEA List, 18 November • Computer Science Department, Dresden University of Technology, 22 September • LIX, École polytechnique, 15 March • LIPN, Univ of Paris 13, 17 March • Institut d’Informatique, Facultés Universitaires Notre-Dame de la Paix, Namur, Belgium, 24 February • LSV, ENS Cachan, 18 Feburary • INRIA Rocquencourt, 17 January
2002: IIT Delhi, 10 December • INRIA Sophia Antipolis, 26 March • DIP, Universitá di Firenze, 8 March • LIP, ENS/Lyon, 22 February • Logic and Interaction Meeting, CIRM, Luminy, 18, 25 February.
2001: INRIA Rocquencourt, 22 May. • LRI, CNRS-Université de Paris Sud, 19 November. • Departamento de Informatica, Pontificia Universidade Catolica do Rio de Janeiro (PUC-Rio), Brazil, 13 December.
2000: LIPN, Institut Galilee, University of Paris 13, 15 December. • LFCS, Edinburgh University, 6 December. • Computer Science Department, Dresden University of Technology, 30 November. • INRIA Rocquencourt, 17 July.
1999: Penn State Logic Seminar, 28 September, 5 October.
1998: Penn State Logic Seminar, 5 May.
1997: Department of Computer Science, University of Chicago, 8 October. • DMI, Ecole Normale Superieure, Paris, 13 January.
1996: Dipartimento di Informatica e Scienze dell’Informazione, Genoa, Italy, 11 December. • Research seminar on “The Mechanization of Inference”, Ohio State University, 26 November. • Department of Computer Science, SUNY Stony Brooks, 20 May. • Department of Mathematics, Wesleyan University, 16 May. • Department of Computer Science, Portland State University, 12 April. • Department of Computer Science, Oregon Graduate Institute, 10 April. • Department of Computer Science, University of Auckland, 9 February. • Unit of Information Technology, University of Technology, Sydney, 7 February. • Royal Melbourne Institute of Technology, Melbourne, 25 January. • Department of Mathematics, University of Siena, 9 January.
1995: Department of Mathematics, University of Padua, 2 June. • University of Pisa, Italy, 9 June. • Dpto. de Lenguajes y Ciencias de la Computacion, Universidad de Malaga, 22 May. • Department of Computer Science, University of Edinburgh, 26 May.
1994: Computer Science Department, Penn State University, December. • Computer Science Department, Duke University, November. • INRIA, Rocquencourt, France, July. • Irisa, Rennes, France, July. • Dipartimento di Informatica e Scienze dell’Informazione, Genoa, Italy, June. • School of Computer Science, Carnegie Mellon University, February.
1992: Computer Science Department, Simon Fraser University, November. • Computer and Information Science, Syracuse University, 20 March. • State University of New York at Buffalo, 30 April. • Swarthmore College, 12 February.
1991: Edinburgh University, Computer Science Department, 24 September. • Glasgow University, Department of Computing Science, 23 September. • Turing Institute, Glasgow, 7 August. • Edinburgh University, Artificial Intelligence Department, 12 May. • Edinburgh University, Cognitive Science Department, 7 March. • University of Oxford, Programming Research Group, 21 February. • University of Cambridge, Computing Laboratory, 20 February. • Edinburgh University, Computer Science Department, 25 January.
1990: Chinese University of Hong Kong, Department of Computer Science, 11 December. • Glasgow University, Department of Computing Science, 29 October. • Edinburgh University, LFCS, 26 October. • St. Andrews University, Scotland, 25 October. • SRI International, 12, 14 March. • Stanford University, CA, 13 March.
1989: Univeristy of Cambridge, Cambridge, UK, 13 December. • Bristol University, Bristol, UK, 12 December. • IBM Research, Hawthorn NY, 7 September. • Swedish Institute of Computer Science, 18 May. • Carnegie Mellon University, 27 April. • ECRC, Munich, Germany, 7 March. • Siemans AG, Munich, Germany, 6 March. • University of Tübingen, Germany, 4 March. • University of Torino, Italy, 2 March. • University of Milano, Italy, 28 February and 1 March. • University of Pisa, Italy, 27 February. • IASI Rome, Italy, 21 February. • University of Rome, Italy, 20 February.
1988: Unisys, Paoli PA, 6 April. • INRIA, Rocquencourt France, 14 March. • University of Cambridge, Computer Laboratory, 9 March. • Imperial College, Computer Science Department, 8 March. • University of Edinburgh, Cognitive Science Department, 3 March. • University of Edinburgh, Computer Science Department, 2 March. • University of Edinburgh, Computer Science Department, 1 March. • University of Glasgow, Computer Science Department, 29 February.
1987: Digital Equipment Corporation, Hudson, MA, 13 October. • SUNY at Stony Brook, Computer Science Department, 18 September. • AT&T Bell Labs, Murray Hill, 12 February.
1986: Columbia University, Computer Science Department, 29 October. • Hong Kong University, Computer Science Department, 5 August. • University of Cambridge, Computer Science Laboratory, 23 July. • University of Edinburgh, Cognitive Science Department, 9 July. • Rutgers University, Computer Science Colloquium, 6 March. • Carnegie Mellon University, Logic Colloquium, 13 February. • MCC, Austin, Texas, 6 February.
1985: SDC Unisys, Paoli, PA, 12 December. • Electrotechnical Laboratory, Ibaraki Japan, 4 June. • Kyoto University, Kyoto Japan, 30 May. • Mid-Atlantic Logic Conference, Philadelphia, PA, 17 February.
1984: Hewlett-Packard, Palo Alto, CA, 23 January.

Workshop and Conference Program Committees

2012: LAM 2012: Fifth International Workshop on Logics, Agents, and Mobility 2011, June, Hamburg, Germany. • LPAR-18: The 18th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. Merida, Venezuela, 11-15 March. • FICS 2012: Fixed Points in Computer Science (a satellite workshop of ETAPS 2012), Tallinn, Estonia, 24 March (Program Committee co-Chair). • IJCAR 2012: International Joint Conference on Automated Reasoning, Manchester, UK, June (Program Committee co-Chair).
2011: LAM 2011: Fourth International Workshop on Logics, Agents, and Mobility, 10 September, Aachen, Germany. • MLPA-11: Modules and Libraries for Proof Assistants, 26 August, Nijmegen. • LICS 2011: Logic in Computer Science, 21-24 June, Toronto. • Tableaux 2011: 20th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, July 4-8, Bern, Switzerland.
2010: LPAR-17: 17th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Yogyakarta, Indonesia, 11-15 October. • Workshop on Proof Systems for Program Logics, FLoC 2010, Edinburgh, 10 July. • Workshop on Logics for Agents and Mobility, FLoC 2010, Edinburgh, 15 July. • Workshop on Proof-Search in Type Theories, FLoC 2010, Edinburgh, 15 July. • Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS), 5 July. • IFIP-TCS 2010: International Conference on Theoretical Computer Science, part of the World Computer Congress in Brisbane, 20-23 September.
2009: Workshop on Games, Dialogue and Interaction, 28-29 Sept, Université Paris 8. • LAM 2009: Logics for Agents and Mobility, August, Los Angeles. A workshop associated to LICS09. • GaLoP IV: Games for Logic and Programming Languages, 28 - 29 March, York, UK. • CSL 2009: 18th Annual Conference of the European Association for Computer Science Logic, 7-11 September, Coimbra, Portugal. • LSFA 2009: Fourth Logical and Semantic Frameworks, with Applications, part of RDP 2009, 28 June-3 July, Brasília, Brazil. • ICALP 09: International Colloquium on Automata, Languages and Programming, Rhodes, Greece, July.
2008: PPDP 2008: 10th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, Valencia, 15-17 July. • ESHOL 2008: Evaluation of Systems for Higher Order Logic, part of IJCAR 2008, Sydney, Australia, 10-15 August. • LAM 2008: Logics for Agents and Mobility Workshop, part of ESSLLI 2008, Hamburg, Germany, 4-15 August. • LSFA08: Third Workshop on Logical and Semantic Frameworks with Applications, Brazil. • CSL08: 17th Annual Conference of the European Association for Computer Science Logic, 15-20 September, Bertinoro, Italy. • TCS 2008: 5th IFIP International Conference on Theoretical Computer Science, August. • FOSSACS 2008: Foundations of Software Science and Computation Structures. Budapest, Spring. • FLOPS 2008: Ninth International Symposium on Functional and Logic Programming, 14-16 April, Ise, Japan.
2007: LFMTP’07: Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, August, Bremem, Germany. • WoLLIC’07: Fourteenth Workshop on Logic, Language, Information and Computation, Rio de Janeiro, 2-5 July. • CADE-21: 21st Conference on Automated Deduction, 17 - 20 July Bremen, Germany.
2006: FSTTCS’06: Foundations of Software Technology and Theoretical Computer Science, Kolkata, India. 13-15 December. • LPAR-13: 13th International Conference on Logic for Programming Artificial Intelligence and Reasoning, Phnom Penh, Cambodia. 13-17 November. • LFMTP’06: Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 16 August. • TFIT’06: Taiwanese-French Conference on Information Technology, Nancy, France. 28-30 March. • Geocal Workshop on Logic Programming and Concurrency, 27 February - 3 March, CIRM, Luminy, France (Program Committee co-Chair)
2005: MoVeLog’05: A Workshop on Mobile Code Safety and Program Verification Using Computational Logic Tools. Barcelona, Spain, 5 October. • LPAR-11: 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. Montevideo, Uruguay, 14-18 March • CSL05: 14th Annual Conference of the European Association for Computer Science Logic, 22-25 August, Oxford, UK • CADE-20: Conference on Automated Deduction, Tallinn, Estonia, 22-27 July.
2004: ICLP’04: Twentieth International Conference on Logic Programming, Saint-Malo, France, 6-9 September. • LFM04: Fourth International Workshop on Logical Frameworks and Meta-Languages.
2003: ACM-Sigplan PPDP03: International Conference on Principles and Practice of Declarative Programming. Uppsala, Sweden. August. (Program Committee Chair). • DCFS 2003: 5th Workshop on Descriptional Complexity of Formal Systems, 12-14 July, Budapest, Hungary. • LPAR 2003: 10th International Conference on Logic for Programming Artificial Intelligence and Reasoning, 22-26 September, Almaty, Kazakhstan. • Merlin 2003: Mechanized Reasoning about Languages with Variable Binding, Uppsala, Sweden, August. • SBLP 2003: 7th Brazilian Symposium on Programming Langauges, Ouro Preto, Minas Gerais, Brazil, 28 - 30 May.
2002: DCFS02: Descriptional Complexity of Formal Systems, 4th Workshop, August 21 - 25, 2002, London, Ontario, Canada. • SBLP 2002: 6th Brazilian Symposium on Programming Langauges, PUC-Rio, Rio de Janeiro, 5-7 June. • PPDP02: International Conference on Principles and Practice of Declarative Programming. Pittsburgh, 6-8 October 2002. • CSL02: 11th Annual Conference of the European Association for Computer Science Logic, 22-25 September. • ICLP02: International Conference on Logic Programming, Copenhagen, 29 July - 2 August, part of FLOC 2002. • CADE02: Conference on Automated Deduction, Copenhagen, 29 July - 2 August, part of FLOC 2002. • LFM02: Logical Frameworks and Meta-languages.
2001: Dagstuhl Seminar on Proof Theory in Computer Science (01411), October 7-12. • ICoS3: Inference in Computational Semantics, 18-19 June. • FLOPS 2001: 5th International Symposium on Functional and Logic Programming, Waseda University, Tokyo, 7-9 March.
2000: CONCUR2000: 11th International Conference on Concurrency Theory, August 22-25, Pennsylvania State University. Conference co-Organizer and PC member. • ICoS-2: Inference in Computational Semantics, Dagstuhl, Germany, 29-30 July. • TABLEAUX’2000: the International Conference on Tableaux and Related Methods, University of St. Andrews, June.
1999: ICALP 99: International Colloquium on Automata, Languages and Programming, Prague, 11 – 15 July 1999. • TABLEAUX’99, the International Conference on Tableaux and Related Methods, Saratoga Springs, NY, June 1999. • ICLP’99: International Conference on Logic Programming, Las Cruces, New Mexico, November 1999.
1998: LICS 98: Logic in Computer Science, 21 - 24 June 1998, Indianapolis. • First Workshop on Component-Based Software Development in Computational Logic, Pisa, 14 (or 18) September.
1997: PLILP 97: International Conference on Programming Languages, Implementations, and Logic Programming, Southampton, UK, September. • ICLP 97: International Conference on Logic Programming, Sydney, Australia, 8-12 July. • CATS 97: Computing: The Australasian Theory Symposium, Sydney, Australia, 3-7 February.
1996: JICSLP 96: Joint International Conference and Symposium on Logic Programming, Bonn, Germany, November. • PLILP 96: International Conference on Programming Languages, Implementations, and Logic Programming, Aachen, Germany, September. • WELP’96: Workshop on Extensions to Logic Programming, 28 – 30 May, Leipzig, Germany.
1995: LICS 95: Logic in Computer Science, 25 – 29 June, San Diego, California.Portland Oregon, December. • ILPS 95: International Symposium on Logic Programming,
1994: POPL 94: The 21st Annual ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages, January. • ASL 94: Annual Meeting of the Association of Symbolic Logic, March, Gainsville Florida. • ICCL 94: International Conference on Constraints in Computational Logics, 7 – 9 September, Munich, Germany.
1993: LICS 93: Logic in Computer Science, 20 – 23 June, Montreal, Quebec. • LPAR 93: International Conference on Logic Programming and Automated Reasoning, St. Petersburg, July. • ILPS 93: International Symposium on Logic Programming, Vancouver, November (Program Committee Chair). • Linear Logic Workshop, Cornell University, June.
1992: JICSLP 92: Joint International Conference and Symposium on Logic Programming, Washington DC, November. • Workshop on Linear Logic and Logic Programming, 14 November (Program Committee Chair). • Workshop on the λProlog programming language, Philadelphia, August (Program Committee Chair). • LPAR 92: International Conference on Logic Programming and Automated Reasoning, St. Petersburg, July. • FGCS92: International Conference on Fifth Generation Computer Systems, 1992. Tokyo, Japan, 1 – 5 June. • META92: Third International Workshop on Meta-programming and Logic.
1990: CADE–10: Tenth International Conference on Automated Deduction, Kaiserslautern, Germany, 23 – 27 July. • Kleene’90: Third Logic Biennial, Bulgaria, 6 – 15 June. • Workshop on Structuring Disciplines for Logic Programming, 15 June, Eilat, Israel (Program Committee Chair). • META90: Second International Workshop on Meta-programming and Logic, April, Leuven, Belgium.
1989: ICLP89: Sixth International Conference on Logic Programming, August, Lisbon Portugal.

Editorial Duties

ACM Transactions on Computational Logic (ToCL). Editor-in-Chief since 1 June 2009; Area editor for Proof Theory since 1999.
Journal of Automated Reasoning, published by Springer. Member of Editorial Board since 2011.
Journal of Applied Logic, published by Elsevier. Area editor for “Type Theory for Theorem Proving Systems” since 2003.
Journal of Logic and Computation, published by Oxford University Press. Associate editor since 1989.
Journal of Functional and Logic Programming, published by European Association for Programming Languages and Systems (EAPLS). Permanent member of the Editorial Board. 1996 – 2010.
Theory and Practice of Logic Programming, published by Cambridge University Press. Editorial Advisor. 1999 – 2009.
Journal of Logic Programming, published by Elsevier Science. Editorial Advisor. 1990 – 1999.

Professional Duties

Organizer of the Special Session on Structural Proof Theory and Computing at the 2012 Annual Meeting of the Association of Symbolic Logic (ASL), Madison, Wisconsin, 31 March - 3 April 2012.
Organizer of a panel on Proof Certificates at Certified Programs and Proofs (CPP), 7 December 2011, Kenting, Taiwan.
Member of the TABLEAUX conference Steering Committee, 2011-2112.
Member of the IJCAR (International Joint Conference of Automated Reasoning) Steering Committee, 2011-2112.
Program committee co-chair for IJCAR 2012: International Joint Conference of Automated Reasoning, Manchester, UK, June 2012.
Program Committee co-Chair for FICS 2012: Fixed Points in Computer Science (a satellite workshop of ETAPS 2012), Tallinn, Estonia.
Member of the selection jury for the 2011 and 2012 E. W. Beth Dissertation Award of the Association for Logic, Language and Information.
Member of a panel of experts charged with the evaluation of research at the University of Uppsala, Sweden, May 2011.
Member of the “comité d’enseignement et recherche du Département d’Informatique de l’X (DIX),” starting October 2010.
Member of the “comité de sélection sur le poste 27PR90 ‘Logique et vérification’ à Rennes 1”, May 2010.
Member of the “comité de programmes,” Digiteo, January 2010 - September 2011.
Co-organizer of 2009 Workshop on Proof-Search in Type Theories (PSTT), 3 August 2009, a CADE 2009 affiliated workshop, Montreal, Canada.
INRIA Saclay hiring committee for CR2, Spring 2008.
Program co-chair for the Geocal Workshop on Logic Programming and Concurrency, 27 Feb - 3 Mar 2005, CIRM, Luminy, France.
Organizing Committee for MoVeLog’05: A Workshop on Mobile Code Safety and Program Verification Using Computational Logic Tools. An ICLP’05 Workshop,Barcelona, Spain, Oct. 5, 2005.
Scientific Committee for the “Spring School on Security”, Marseille, France, 25-29 April 2005.
Elected twice to the Executive Council of the Association for Logic Programming: once for four years starting January 1991 and once for four years starting January 2005.
Member of the “comite d’evaluation” of the PPS (Preuves, Programmes et Systemes) lab operated jointly by CNRS and University Paris 7, November 2003.
Program Committee Chair for International Conference on Principles and Practice of Declarative Programming (PPDP 2003). Uppsala, Sweden. August 2003.
Member of Concurrency Working Group during the Strategic Directions in Computer Research (SCDR), 14-15 June 1996, Boston. Sponsored by the ACM.
Member of Steering committee for the International Conference on Principles and Practice of Declarative Programming (PPDP).
Member of Working Group on Software Engineering and Programming Language, 12-13 June 1996, Boston. Sponsored by the NSF and Army Research Office.
Organizing Committee for LICS (Logic in Computer Science), 1993 – 1998.
Tutorial Chair for CONCUR’95, Philadelphia, August 1995.
Program Committee Chair for the International Symposium on Logic Programming, Vancouver, November 1993.
Program Committee Chair for the Workshop on Linear Logic and Logic Programming, Washington DC, 14 November 1992.
Program Committee Chair for the Workshop on the λProlog programming language, Philadelphia, August 1992.
Program Committee Chair for the Workshop on Structuring Disciplines for Logic Programming, Eilat, Israel, 15 June 1990.

Distinctions

LICS Test-of-Time Award 2011 for a paper co-authored with Joshua Hodas from LICS 1991.
“La prime d’excellence scientifique” (PES) from INRIA for 2010-2013.
Finalist in the 33^rd Westinghouse Science Talent Search (now the Intel Science Talent Search), 1974.

External Examiner

External Examiner for PhDs after 2010: Robert Simmons, Carnegie Mellon University (planned). • Sean McLaughlin, Carnegie Mellon University (planned). • Nicolas Pouillard, University of Paris 7, 13 January 2012 (rapporteur). • Anders Starcke Henriksen, University of Copenhagen, December 2011. • Francois Garillot, Ecole Polytechnique, 5 December 2011. • Daniel Weller, Technische Universität Wien, 12 January 2011.
External Examiner for PhDs during 2000-2010: • Elie Soubiran, Ecole Polytechnique (examinateur) 27 September 2010. • Clement Houtmann, Nancy, 12 March 2010 (examinateur). • Denis Cousineau, Ecole Polytechnique, 1 Dec 2009 (examinateur). • Xiaochu Qi, Computer Science Department, University of Minnesota, 9 September 2009 (external examiner). • Andrew Gacek, Computer Science Department, University of Minnesota, 8 September 2009 (external examiner). • Samuel Mimram, Université Paris VII, 1 December 2008 (examinateur). • Paolo Di Giamberardino, University of Rome 3 and University of the Mediterranean, 18 April 2008 (examinateur). • Sébastien Briais, École Polytechnique Fédérale de Lausanne, 17 Dec 2007 (rapporteur). • Stéphane Lengrand, Université Paris VII & University of St Andrews, 8 Dec 2006 (examinateur). • Nicolas Oury, LRI, University of Paris Sud, 15 September 2006 (examinateur). • James Brotherston, LFCS, University of Edinburgh, 6 September 2006 (external examiner). • Gabriele Pulcini, University of Rome 3, 28 April 2006 (rapporteur). • Sylvain Salvati, Institut National Polytechnique de Lorraine, 13 June 2005 (examinateur). • Didier Le Botlan, INRIA-Rocquencort, École polytechnique, 6 May 2004 (examinateur). • Sorin Craciunescu, INRIA-Rocquencort, École polytechnique, March 2004 (rapporteur). • Kumar Neeraj Verma, LSV, ENS-Cachan, September 2003 (examinateur). • Kai Brünnler, Department of Computer Science, TU Dresden, September 2003. • Veronique Cortier, LSV, ENS-Cachan, March 2003 (rapporteur). • Remi Baudot, University of Paris 13, December 2000 (rapporteur). • Alberto Momigliano, Carnegie Mellon, July 2000.
External Examiner for PhDs before 2000: • Ernie Ong, University of Western Australia, December 1997. • Alain Hui-Bon-Hoa, University of Paris VII, December 1997. • Giorgio Delzanno, University of Genoa, December 1996. • Alessio Guglielmi, Computer Science Department, Pisa, December 1995. • Keehang Kwon, Computer Science Department, Duke University, November 1994. • Scott Dietzen, School of Compter Science, Carnegie Mellon University, March 1992. • Francesca Arcelli, Dip. Scienze dell’Informazione, Universita‘ di Milano, July 1991. • Jean-Marc Andreoli, Thèse d’Informatique de l’Universitè de Paris 6, France, June 1990. • Andrea Corradini, Computer Science Department, University of Pisa, January 1990. • Remo Pareschi, Cognitive Science Department, University of Edinburgh, March 1988. • Sanjay Manchanda, Department of Computer Science, State University of New York at Stony Brook, September 1987.
Evaluation of Habilitation: Agata Ciabattoni, March 2007. • Gilles Barthe, June 2004. • Delia Kesner, Nov 2001. • Jean-Marc Andreoli, May 2001.
External expert for the selection of a Professor in Theoretical Computer Science, Goteborg, Sweden.
Member of a Review Panel (28 November 2006) for Graduate Schools and for Clusters of Excellence, Deutsche Forschungsgemeinschaft (German Research Foundation).
Referee for Trinity College Fellowship Election, Cambridge.
Research Initiation Awards panel for NSF.
Reviewer of application for Senior Research Fellowship, EPSCR, UK.

Ph.D. Dissertation Supervision

In progress: Ivan Gazeau and Anne-Laure Schneider.
Olivier Delande, “Symmetric Dialogue Games in the Proof Theory of Linear Logic,” 15 October 2009, Ecole Polytechnique.
Vivek Nigam, “Exploiting non-canonicity in the sequent calculus,” 18 September 2009, Ecole Polytechnique.
David Baelde, “A linear approach to the proof-theory of least and greatest fixed points,” 9 December 2008, Ecole Polytechnique.
Alexis Saurin, “Une étude logique du contrôle,” 30 September 2008, Ecole Polytechnique. His thesis won the “Prix de thèse de l’Ecole Polytechnique” and the “Prix de thèse ASTI 2009”.
Alwen Tiu, “A Logical Framework for Reasoning about Logical Specifications,” 15 March 2004, Pennsylvania State University.
Jérémie Wajs, “Reasoning about logic programs using definitions and induction”, 10 May 2002, Pennsylvania State University.
Elaine Pimentel, “Linear logic as a framework for specifying sequent calculus” December 2001, Department of Computer Science, Universidade Federal de Minas Gerais, Brazil. Co-advised with Carlos Camarão de Figueiredo.
Ray McDowell, “Reasoning in a Logic with Definitions and Induction,” September 1997, University of Pennsylvania.
Chuck Liang, “Object-language substitution and unification in meta-logic,” September 1995, University of Pennsylvania.
Jawahar Lal Chirimar, “Proof Theoretic Approach To Specification Languages,” February 1995, University of Pennsylvania.
Joshua Hodas, “Logic Programming in Intuitionistic Linear Logic: Theory, Design, and Implementation,” August 1993, University of Pennsylvania.
John Hannan, “Proof-theoretic methods for analysis of functional programs,” August 1990, University of Pennsylvania.
Amy Felty, “Implementing theorem provers in a higher-order logic programming language,” August 1989, University of Pennsylvania.
Gopalan Nadathur, “A higher-order logic as the basis for logic programming,” December 1986, University of Pennsylvania.

Master’s Thesis Supervision

Jérémie Wajs, “Design and implementation of a theorem prover for operational semantics”, May 2000.
Alexander Betis, “Object Programming, Linear Logic and Java”, December 1999.
Joshua Hodas, “Object-Oriented Programming in Logic Programming,” May 1990.
Amy Felty, “Using extended tactics to do proof transformations,” December 1986.
Greg Hager, “Computational aspects of proofs in modal logic,” December 1985.

International Visitors Hosted at the Pennsylvania State University

Alexis Saurin, Spring and Summer 2002. A five month research training period as part of his degree at the Ecole Normale Supérieure de Paris.
Emmanuel Jeandel, Summer 2001. A ten-week research training period as part of his Master of Computer Science (Magistère d’Informatique et Modélisation) at the Ecole Normale Supérieure de Lyon.
Elaine Pimentel, September 1999 - Feburary 2001. PhD student, Brazil.
Luis Pinto, 28 August - 26 September 1998. Assistant Professor from the University of Minho, Portugal.
Pablo Lopez, 7 September - December 3 1998. PhD student at the University of Malaga, Spain.

International Visitors Hosted at the Unversity of Pennsylvania

Christian Urban, 9 May – 2 June 1996. PhD student from the University of St. Andrews, Scotland.
Robert Stärk, January – June 1996. Post doc from Universität München traveling on a Swiss National Science Foundation grant.
Giorgio Delzanno, 4 March – 25 May 1995. PhD student from the University of Genova.
Ernesto Pimentel, 1 December 1994 – 28 February 1995. Professor from the University of Malaga.
Catuscia Palamidessi, July – August 1994. Professor from the University of Genova.
Alessio Guglielmi, 15 February – 30 May 1994. PhD student from the University of Pisa.
Alain Hui-Bon-Hoa, 1 December 1992 – 30 March 1994. PhD student from the University Paris VII.
Philippa Gardner, September – December 1992. PhD student from Edinburgh University.
James Harland, January – February 1988. PhD student from Edinburgh University.
Jean-Yves Girard, October – November 1987. Professor from the University Paris VI.

Supervised Post Docs and Staff

Beniamino Accattoli, post doc at INRIA, from Sep 2011 to Aug 2012.
Clément Houtmann, post doc at INRIA, from Sep 2010 to Aug 2010.
Andrew Gacek, post doc at INRIA, from Oct 2009 to Sep 2010.
Kaustuv Chaudhuri, post doc at INRIA, from Oct 2006 to Sep 2006.
Murdoch Gabbay, post doc at INRIA, from July 2003 to July 2004.
Kamal Aboul-Hosn, programmer and junior research assistant, Spring 2002.
Philip Wickline, staff programming working on λProlog implementation for a year starting July 1995.
Elsa Gunter, post doc from September 1987 to August 1988.

Publications

Refereed Journal Publications

“A two-level logic approach to reasoning about computations” with Andrew Gacek and Gopalan Nadathur. Accepted to the Journal of Automated Reasoning in June 2010.
“A Focused Approach to Combining Logics” with Chuck Liang. Annals of Pure and Applied Logic, 162 (2011), pp. 679-697.
“Nominal abstraction” with Andrew Gacek and Gopalan Nadathur. Information & Computation, 209, 2011, pp. 48-73.
“A framework for proof systems,” with Vivek Nigam. Journal of Automated Reasoning, 45(2), 2010, pp. 157-188.
“Proof Search Specifications of Bisimulation and Modal Logic for the π-calculus”, with Alwen Tiu. ACM Transactions on Computational Logic, 11(2), 2010.
“Proof and refutation in MALL as a game,” with Olivier Delande and Alexis Saurin. Annals of Pure and Applied Logic, 161(5), February 2010, pp. 654-672.
“Focusing and Polarization in Linear, Intuitionistic, and Classical Logics,” with Chuck Liang. Theoretical Computer Science, 410(46), 2009, pp. 4747-4768.
“A Proof Theory for Generic Judgments,” with Alwen Tiu. ACM Transactions on Computational Logic, 6(4), October 2005, pp. 749–783.
“Encoding Transition Systems in Sequent Calculus,” with Raymond McDowell and Catuscia Palamidessi. Theoretical Computer Science, 294(3), pp. 411-437 (2003).
“Reasoning with Higher-Order Abstract Syntax in a Logical Framework” with Raymond McDowell. ACM Transaction on Computational Logic, Vol. 3(1), 80-136 (2002).
“Cut-Elimination for a Logic with Definitions and Induction,” with Raymond McDowell. Theoretical Computer Science, Vol. 232, pages 91 - 119 (2000).
“Foundational Aspects of Syntax,” with Catuscia Palamidessi. ACM Computing Surveys Symposium 31(3es):11 (1999). Ed. by Pierpaolo Degano, Roberto Gorrieri, Alberto Marchetti-Spaccamela, and Peter Wegner.
“Forum: A multiple-conclusion specification logic”. Theoretical Computer Science, 165(1): 201-232 (1996).
“Logic programming in a fragment of intuitionistic linear logic,” with Joshua Hodas. Information and Computation, 110(2), 327-365 (1994).
“From operational semantics to abstract machines” with John Hannan. Mathematical Structures in Computer Science, 2(4), 415 – 459 (1992).
“Unification under a mixed prefix.” J. of Symbolic Computation, Vol. 14, 321 – 358 (1992).
“A logic programming language with lambda-abstraction, function variables, and simple unification,” J. of Logic and Computation, 1(4), 497 – 536 (1991).
“Uniform proofs as a foundation for logic programming” with Gopalan Nadathur, Frank Pfenning, and Andre Scedrov, Annals of Pure and Applied Logic, Vol. 51, 125 – 157 (1991).
“Higher-order Horn clauses” with Gopalan Nadathur, J. of the ACM, 37(4), 777 – 814 (1990).
“A logical analysis of modules in logic programming,” J. of Logic Programming, 6 (1989), 79 – 108. Translated to Russian and reprinted in Mathematical Logic in Programming, edited by Y. I. Janov, M. V. Zakhar’yashchev, and A. Voronkov (Mir Publishers, USSR, 233 – 273 (1991)).
“A compact representation of proofs,” Studia Logica, 46(4), 345 – 368 (1987).
Refereed Conference and Workshop Publications
“A non-local method for robustness analysis of floating point programs” with Ivan Gazeau and Catuscia Palamidessi. Accepted to QAPL 2012: Tenth Workshop on Quantitative Aspects of Programming Languages, 31 March - 1 April 2012, Tallinn, Estonia.
“A proposal for broad spectrum proof certificates.” CPP 2011: First International Conference on Certified Proofs and Programs, 7-9 December 2011, Taiwan, December 2011. LNCS 7086, pp. 54-69.
“Reasoning about computations using two-levels of logic.” APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, Shanghai Jiao Tong University, China, 28 November - 1 December 2010. LNCS 6461, pp. 34-46.
“Focused inductive theorem proving,” with David Baelde and Zachary Snow. IJCAR: International Joint Conference on Automated Reasoning, July 2010, Edinburgh. LNCS 6173, pp. 278-292.
“Finding Unity in Computational Logic.” ACM-BCS Visions of Computer Science 2010 conference, 13-16 April 2010.
“Algorithmic specifications in linear logic with subexponentials,” with Vivek Nigam. PPDP 2009: International Conference on Principles and Practice of Declarative Programming, pp. 129–140, Coimbra, Portugal, 7-9 September 2009.
“A Unified Sequent Calculus for Focused Proofs,” with Chuck Liang. LICS 2009: 24th Symp. on Logic in Computer Science, June 2008, pp. 355–364, Los Angeles, 11-14 August 2009.
“Reasoning in Abella about Structural Operational Semantics Specifications,” with Andrew Gacek and Gopalan Nadathur. LFMTP 2008: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Pittsburgh, June 2008, pp. 75–89.
“Canonical Sequent Proofs via Multi-Focusing,” with Kaustuv Chaudhuri and Alexis Saurin. Proceedings of the IFIP International Conference on Theoretical Computer Science, September 2008, pp. 383–396.
“Focusing in linear meta-logic,” with Vivek Nigam. Proceedings of IJCAR 2008: International Joint Conference on Automated Reasoning, Sydney, August 2008, LNCS 5195, pp. 507–522.
“A neutral approach to proof and refutation in MALL,” with Olivier Delande. LICS 2008: 23th Symp. on Logic in Computer Science, June 2008, pp. 498–508.
“Combining generic judgments with recursive definitions,” with Andrew Gacek and Gopalan Nadathur. LICS 2008: 23th Symp. on Logic in Computer Science, June 2008, pp. 33–44.
“Least and greatest fixed points in linear logic” with David Baelde. LPAR 2007: International Conference on Logic for Programming and Automated Reasoning, LNCS 4790, pp. 92-106.
“Focusing and Polarization in Intuitionistic Logic” with Chuck Liang. CSL07: Computer Science Logic 2007. LNCS 4646, pp. 451-465.
“Incorporating tables into proofs” with Vivek Nigam. CSL07: Computer Science Logic 2007. LNCS 4646, pp. 466-480.
“From proofs to focused proofs: a modular proof of focalization in Linear Logic” with Alexis Saurin. CSL07: Computer Science Logic 2007. LNCS 4646, pp. 405-419.
“The Bedwyr system for model checking over syntactic expressions” with David Baelde, Andrew Gacek, Gopalan Nadathur, and Alwen Tiu. A system description in CADE21: Conference on Automated Deduction 2007. LNAI 4603, 391-397.
“Representing and reasoning with operational semantics.” Proceedings of IJCAR’06 (Third International Joint Conference on Automated Reasoning), 17 - 20 August 2006, Seattle.
“Collection analysis for Horn clause programs.”. Proceedings of the Eighth ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming (PPDP’06), Venice, Italy, 10-12 July 2006
“Mixing Finite Success and Finite Failure in an Automated Prover,” with Alwen Tiu and Gopalan Nadathur. Proceedings of ESHOL’05: Empirically Successful Automated Reasoning in Higher-Order Logics, December 2005.
“On the specification of sequent systems,” with Elaine Pimentel. Proceedings of LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. 2 - 6 December, Montego Bay, Jamaica.
“A congruence format for name-passing calculi,” with Axelle Ziegler and Catuscia Palamidessi. Proceedings of SOS05: Structural Operational Semantics, 2005.
“A game semantics for proof search: Preliminary results,” with Alexis Saurin. Proceedings of Mathematical Foundations of Programming Semantics, 2005.
“Linear Logic as a Framework for Specifying Sequent Calculus,” with Elaine Pimentel. Logic Colloquium 1999. Ed. Jan Van Eijck, Vincent Van Oostrom, and, Albert Visser. Published by the Association for Symbolic Logic, 111-135 (2004).
“A Proof Search Specification of the π-Calculus”, with Alwen Tiu. Proceedings of the 2004 Foundations of Global Ubiquitous Computing, edited by Julian Rathke, London, September (ENTCS).
“A Proof Theory for Generic Judgments: An extended abstract,” with Alwen Tiu. Proceedings of the 2003 Symposium on Logics in Computer Science, edited by Phokion Kolaitis, Ottawa, July 2003. pp. 118-127.
“Encryption as an Abstract Data-Type: An extended abstract,” Proceedings of FCS’03: Foundations of Computer Security, edited by Iliano Cervesato, pp. 3-14, June 2003.
“Encoding Generic Judgments” with Alwen Tiu. Proceedings of FSTTCS 2002 (22nd Foundations of Software Technology and Theoretical Computer Science), edited by M. Agrawal and A. Seth.
“Higher-order quantification and proof search.” Proceedings of AMAST 2002, LNCS 2422, edited by Hélène Kirchner and Christophe Ringeissen. pp. 60-74.
“Using linear logic to reason about sequent systems,” with Elaine Pimentel. Proceedings of Tableaux 2002, LNCS, edited by Uwe Egly, Christian G. Fermüller.
“Encoding generic judgments: Preliminary results,” Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN 2001), Siena, Italy, June 18, 2001, in connection with IJCAR 2001. To appear in the Electronic Notes of TCS.
“Abstract Syntax for Variable Binders: An Overview.” Proceedings of Computational Logic - CL2000, pp. 239-253, July 2000, edited by John Lloyd, et. al. Springer-Verlag, LNAI 1861.
“A Logic for Reasoning with Higher-Order Abstract Syntax,” with Raymond McDowell. Proceedings of 1997 Symposium on Logics in Computer Science, Warsaw, 434 – 445.
“Encoding Transition Systems in Sequent Calculus: Preliminary Report,” with Raymond McDowell and Catuscia Palamidessi. Proc. of the Linear Logic Workshop, Tokyo, 29 March - 2 April 1996. Appears in Volume 3 of Electronic Notices of Theoretical Computer Science.
“Logical Foundations for Open System Design,” Computing Surveys 28(4): 48 (1996).
“A Multiple-Conclusion Meta-Logic.” Proc. of the 1994 Symposium on Logics in Computer Science, Paris, 272 – 281.
“The π-calculus as a theory in linear logic: Preliminary results.” Proc. of the 1992 Workshop on Extensions to Logic Programming, edited by E. Lamma and P. Mello. Springer-Verlag, LNCS 660, 242 – 265.
“Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract,” with Joshua Hodas, 1991 Logics in Computer Science, Amsterdam, 32 – 42. Awarded the Test-of-Time award at LICS 2011.
“Unification of Simply Typed Lambda-Terms as Logic Programming,” in the Proc. of the 1991 International Conference on Logic Programming, edited by Koichi Furukawa, June 1991.
“Extending Definite Clause Grammars with Scoping Constructs” with Remo Pareschi, in the Proc. of the 1990 International Conference in Logic Programming, edited by D. H. D. Warren and Peter Szeredi, 373 – 389.
“Representing Objects in a Logic Programming Language with Scoping Constructs” with Joshua Hodas, in the Proc. of the 1990 International Conference in Logic Programming, edited by D. H. D. Warren and Peter Szeredi, 511 – 526.
“From Operational Semantics to Abstract Machines: Preliminary Results” with John Hannan, the Proc. of the 1990 Lisp and Functional Programming Conference, edited by M. Wand, 323 – 332.
“Encoding a Dependent-Type λ-Calculus in a Logic Programming Language” with Amy Felty, the 1990 Conference on Automated Deduction, Springer-Verlag Lecture Notes in Artificial Intelligence, Volume 449, edited by Mark Stickel, 221–235.
“A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification” in Extensions of Logic Programming ed. Peter Schroeder-Heister, Springer-Verlag, Lecture Notes in Artificial Intelligence 475, December 1989, 253 – 281.
“Lexical Scoping as Universal Quantification” in the Sixth International Logic Programming Conference, eds. G. Levi and M. Martelli, Lisbon, Portugal, June 1989, 268 – 283.
“Uses of higher-order unification for implementing program transformers” with John Hannan, Fifth Symposium on Logic Programming, ed. by Kenneth A. Bowen and Robert A. Kowalski, MIT Press, August 1988, Seattle, Washington, 942 – 959.
“An overview of λProlog” with Gopalan Nadathur, Fifth Symposium on Logic Programming, ed. by Kenneth A. Bowen and Robert A. Kowalski, August 1988, Seattle, Washington, 810 – 827.
“Specifying theorem provers in a higher-order logic programming language” with Amy Felty, 9th International Conference on Automated Deduction, ed. Ewing Lusk and Ross Overbeck, Argonne, IL, May 1988, 61 – 80.
“A logic programming approach to manipulating formulas and programs” with Gopalan Nadathur, IEEE Symposium on Logic Programming, San Francisco, September 1987, Program Chair Seif Haridi, 379 – 388.
“Hereditary Harrop formulas and uniform proofs systems” with Gopalan Nadathur and Andre Scedrov, Second Annual Symposium on Logic in Computer Science, Program Chair David Gries, Cornell University, June 1987, 98 – 105.
“A theory of modules for logic programming,” IEEE Symposium on Logic Programming, Salt Lake City, September 1986, Program Chair Robert M. Keller, 106 – 114.
“An integration of resolution and natural deduction theorem proving” with Amy Felty, National Conference on Artificial Intelligence, Philadelphia, August 1986, Program Co-Chairs Tom Kehler and Stan Rosenschein, 198 – 202.
“Higher-order logic programming” with Gopalan Nadathur, Proc. of the Third International Logic Programming Conference, edited by Ehud Shapiro, London, June 1986, 448 – 462.
“Some uses of higher-order logic in computational linguistics” with Gopalan Nadathur, 24th Annual Meeting of the Association for Computational Linguistics, New York, June 1986, 247 – 255.
“Expansion tree proofs and their conversion to natural deduction proofs,” the 7th Conference on Automated Deduction, edited by R. E. Shostak, Lecture Notes in Computer Science, No. 170, Springer-Verlag, 1984, 375 – 393.
“A look at TPS” with P. B. Andrews, Eve L. Cohen, 6th Conference on Automated Deduction, edited by Donald W. Loveland, Lecture Notes in Computer Science, No. 138, Springer-Verlag, 1982, 50 – 69.

Book Chapters
“A Proof-Theoretic Approach to the Static Analysis of Logic Programs” in Reasoning in Simple Type Theory: Festschrift in honour of Peter B. Andrews on his 70th birthday. Edited by Christoph Benzmueller, Chad E. Brown, Jörg Siekmann, and Richard Statman, Studies in Logic, published by College Publications, December 2008.
“Overview of linear logic programming”. In Linear Logic in Computer Science, edited by Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott. Cambridge University Press, London Mathematical Society Lecture Notes Series, volume 316 (2003).
“Sequent Calculus and the Specification of Computation.” In Computational Logic, edited by U. Berger and H. Schwichtenberg. NATO Advanced Science Institute Series, sub-series F: Computer & Systems Science, Springer, 399 – 444. Taken from lectures given at the International Summer School Marktoberdorf on Logic of Computation, 29 July - 10 August 1997.
“Logic Programming and Meta-Logic” in The Logic of Computation, edited by H. Schwichtenberg. NATO Advanced Science Institute Series, sub-series F: Computer & Systems Sciences, published by Springer-Verlag, pp. 265 – 308 (1997). Taken from lectures given at the International Summer School Marktoberdorf on Logic of Computation, 25 July - 6 August 1995.
“Higher-order Logic Programming” with Gopalan Nadathur, Handbook of Logic in Artificial Intelligence and Logic Programming, Volume 5. Edited by Dov M. Gabbay, C. J. Hogger, and J. A. Robinson (Clarendon Press, Oxford), pp. 499 – 590 (1998).
“Abstractions in logic programming,” in Logic and Computer Science, edited by Pieirgiorgio Odifreddi, Academic Press (APIC Series 31) 1990, 329 – 359.
“A Meta-Language for Functional Programming” with John Hannan, in Meta-Programming in Logic Programming, edited by H. Abramson and M. Rogers, MIT Press, Chapter 24, 1989, 453 – 476.
“Automating higher order logic” with Peter B. Andrews, Eve Longini Cohen, and Frank Pfenning, in Automated Theorem Proving: After 25 Years, ed. W. W. Bledsoe and D. W. Loveland, AMS, 1984, 169 – 192.

Other Proceedings
“Observations about using logic as a specification language,” invited paper to the 1995 Gulp-Prode Joint Conference on Declarative Programming, Salerno, Italy, 11 – 14 September 1995.
“A Proposal for Modules for λProlog: Preliminary Draft,” Proc. of the 1992 λProlog Workshop, August 1992.
“Abstract Syntax and Logic Programming,” Proc. of the First and Second Russian Conferences on Logic Programming, September 1991, St. Petersburg, LNAI Series, Springer-Verlag.
“A Meta Language for Type Checking and Inference: An Extended Abstract,” with Amy Felty, Proc. of the 1989 Workshop on Programming Logic, Bålstad, Sweden.
“Deriving mixed evaluation from standard evaluation for a simple functional programming language,” with John Hannan, 1989 International Conference on Mathematics of Program Construction, Program Chair Jan L. A. van de Snepscheut, Springer-Verlag, LNCS 375, 239 – 255.
“A computational logic approach to syntax and semantics,” with Gopalan Nadathur. Invited submission for the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985.

Encyclopedia entries
“Linear Logic” with Roberto DiCosmo. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
“Logic, Higher-order,” article for the Second Edition of the Encyclopedia of Artificial Intelligence, ed. S. Shapiro, 1992.

Newsletters and Bulletins
“Formalizing operational semantic specifications in logic.” Concurrency Column of the Bulletin of the European Association for Theoretical Computer Science (EATCS), October 2008.
“Logic and Logic Programming: A Personal Account”, ALP Newsletter, February 2006, 19(1).
“A Survey of Linear Logic Programming”. Computational Logic: The Newsletter of the European Network in Computational Logic, Volume 2, No. 2, December 1995, pp. 63 - 67.
“Proof Theory as an Alternative to Model Theory,” guest editorial for the Newsletter of the ALP, August 1991.

Published Reviews
Review of Invariants, composition, and substitution, by Ekkart Kindler, Acta Inf. 4 (June 1995), 299-312. Computing Reviews, September 1996.
Review of A computational logic and A computational logic handbook by Robert Boyer and J. Strother Moore, Journal of Symbolic Logic, September 1990, 1302 – 1304.
Review of The art of Prolog: advanced programming techniques, by Leon Sterling and Ehud Shapiro. Computing Reviews, 349 – 350, July 1987.
Review of “Constructive mathematics as a programming logic I: some principles of theory” by Robert Constable. Computing Reviews, April 1987, 213 – 214.

Edited Volumes
Proc. of the 2003 International Conference on Principles and Practice of Declarative Programming (PPDP 2003). Edited by Dale Miller. Published by the ACM.
Logic Programming, Proceedings of the 1993 International Symposium, edited by Dale Miller. Vancouver, British Columbia, Canada, October 26-29, 1993. MIT Press 1993, ISBN 0-262-63152-0.
Proc. of the Workshop on Linear Logic and Logic Programming, Washington, DC, November 1992. Edited by Dale Miller. Available as UPenn CIS technical report MS-CIS-92-80.
Proc. of the Workshop on the λProlog Programming Language, University of Pennsylvania, July 1992. Edited by Dale Miller. Available as UPenn CIS technical report MS-CIS-92-86.

Miscellaneous
“An Extension to ML to Handle Bound Variables in Data Structures,” in the Proc. of the Logical Frameworks BRA Workshop, May 1990.
“Hereditary Harrop formulas and logic programming,” Proc. of the VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow, August 1987 (abstract).
“Higher-order logic programming,” Journal of Symbolic Logic 51(3), p. 851, 1986 (abstract). Talk presented at the meeting on Logic, Language, and Computation, 18 July 1985, Stanford University.
“Expansion tree proofs in higher-order logic,” Journal of Symbolic Logic 49(4), 1984, 1443 – 1444 (abstract). Talk given at the Annual Meeting of the Association for Symbolic Logic, 30 December 1983, Boston.
“The sum of an integer’s digits: some properties,” Journal of Undergraduate Mathematics, September 1976, Vol. 8, 61 – 64.

Books
Programming with higher-order logic, with Gopalan Nadathur, Cambridge University Press. To appear in early 2012.

Departmental and University Service at Penn State

Promotion and Tenure Committee, CSE, 2001-2.
Strategic Committee, CSE, 2001-2.
Department Head of Computer Science and Engineering, September 1997 to August 2001.
Coordinating Council for IST, 1999.
Search Committee for the Dean of the School for IST, 1998.
Building Selection Committee for the new IST/CSE Building, August 1999 to August 2001.
CoE United Way Committee, 1999/2000.
Member of the Information Science and Technology Strategic Planning Group, 1997/98.
Member of the College of Engineering Task Force on Faculty Release Time, Cost Sharing and Overhead, 1997/98.
Member of the Staff Grade Review Committee, College of Engineering, Fall 1999.

Departmental and University Service at UPenn

Selected for a Faculty Service Award in the CIS Department at Penn, June 1994.
Written Preliminary Exam I organizing committee, 1991, 1992, 1993 (chair one year).
CIS Colloquium organizer, 1991, 1992, 1993, 1994, 1995.
Committee on Mathematics Course Offerings in SEAS, 1991, 1992.
Secretary of the CIS Faculty, one year.
CIS Graduate Admissions Committee, several years.
The Computer Science coordinator of the Logic and Computation Seminar, four years.
Undergraduate curriculum committee, two years.
I have supervised 15 graduate students in independent study courses, in the areas of algebra, logic, type theory, theorem proving, denotational semantics, and complexity theory. These have been student that I did not otherwise advise on research.
I have supervised twelve senior project students.
I have served on the PhD committee of at least 15 students at Penn, as well as at least 10 committees for the Written Preliminary Exams Part II.
Member of the Task Force for the Future of Computing at Carnegie Mellon University, chaired by Allen Newell, 1982.

Courses Taught at Ecole polytechnique

INF 431: Informatique Fondamentale (Petit Class), Spring 2003, 2004, 2005, 2006.
INF 542: Automates, langages, calculabilité (Petit Class), Winter 2003, 2004, 2005, 2006.
INF 585: Logics for Computer Science, Spring 2004, 2005, 2006.

Courses Taught at Penn State

CSE 598A, Logic Programming: Advance features and applications, Fall 00.
CSE 428, Programming Language Concepts, Spring 00, 02.
CSE 260, Discrete Mathematics for Computer Science, Fall 00.
CSE 597a, Program Analysis Seminar, Fall 00.
CSE 522, Semantics of Programming Languages, Spring 00.
CSE 468, Theory of Automata, Languages, and Computability. Spring 99.

Courses Taught at UPenn

CSE 120, Programming Languages and Techniques I, Fall 1993, Fall 1995
CSE 220, Design and Analysis of Algorithms, Spring 1986, 1990.
CSE 260, Mathematical Foundations of Computer Science I, Fall 1983, 1984, 1985.
CSE 261, Mathematical Foundations of Computer Science II, Spring 1992.
CSE 360, Logic and Computation, Spring 1994, Spring 1995.
CSE 400/401, Senior Projects, Spring 1988, Fall 1988.
CIS 500, Programming Languages and Techniques, Fall 1986, 1988, 1989.
ENGM 504, Logic and Computation in Algebra, Spring 1992, 1994, 1996, Fall 1994, 1995.
CIS 578, Algebra for Computer Science, Fall 1986, 1987.
Seminar in Computational Logic, Spring 1986.
Seminar in Logic for Logic Programming, Spring 1985.
Seminar in Automatic Theorem Proving, Spring 1984.

This document was translated from L^AT_EX by H^EV^EA.