Dale Miller
Curriculum Vitae
Inria Saclay  ÎledeFrance & Laboratoire d’Informatique, LIX
1 rue Honoré d’Estienne d’Orves
Bâtiment Alan Turing
Campus de l’École Polytechnique
Palaiseau, 91120 France
dale.miller @ inria.fr
http://www.lix.polytechnique.fr/Labo/Dale.Miller/
Phone: (+33) 01 77 57 80 53
Employment

September 2002 – Present: Directeur de Recherche (DRCE since 01.2018), 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

20 April – 20 May 2019: Visiting Fellow, The Australian National University.
 February 2002: Guest professor, University AixMarseille 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. We have two children.
 USA citizen. Titre de séjour, France.
Editorial Duties

ACM Transactions on Computational Logic (ToCL).
Two term EditorinChief, from 1 June 2009 to 30 June 2015.
Also a founding Area Editor (for the area of Proof Theory) 19992018.
 Journal of Automated Reasoning, published by Springer.
Member of Editorial Board since May 2011.
 Journal of Applied Logic, published by Elsevier. Area
editor for “Type Theory for Theorem Proving Systems” since 2003.
 Theory and Practice of Logic Programming, published by
Cambridge University Press. Editorial Advisor from 1999 to 2015.
 Journal of Logic and Computation, published by Oxford
University Press. Associate editor 1989  2012.
 Logical Methods in Computer Science, guest editor for two
special issues on papers selected from CSLLICS 2014 and from FSCD
2017.
Professional Duties

Chair of the Search Committee for the next EditorinChief of
the ACM Transactions on Computational Logic, Spring 2021.
 LICS General Chair starting July 2018 for three years.
Member of the LICS Steering Committee, starting 2012.
Member of the LICS Organizing Board 1994  1997 and 2014  2015.
Chair of the LICS 1995 TestofTime Award selection committee,
August 2014  July 2015.
 Scientific leader of the Parsifal team. Parsifal was an Inria
Saclay team from 20072019 and a LIX team from 20042019.
 Program committee chair for the 2nd International Conference on
Formal Structures for Computation and Deduction (FSCD), Oxford, 36
September 2017.
 Program committee cochair for the workshop on Logical
Frameworks and Meta Languages: Theory and Practice (LFMTP), 2019,
Vancouver, Canada.
 Member of an international review panel for the Distinguished
Professor Grant at the Swedish Research Council, Fall 2017 and Fall
2019.
 Member of the FSCD Steering Committee, September 2017  August
2020.
 Member of the LFMTP Steering Committee, July 2019  June 2024.
 Member of the EATCS Distinguished Dissertation Award Committee
from 2013 to 2019.
 Member of the selection jury for the 2011, 2012, and 2013
E. W. Beth Dissertation Award of the Association for Logic, Language
and Information.
 Member of the Ackermann Award Committee for 2016  2019.
This award is given by EACSL for an outstanding doctoral dissertation
in the field of Logic in Computer Science.
 Member of the 2012, 2016, 2017, 2018, 2019 Herbrand Award
Committee of the Association for Automated Reasoning. Chair of the
2019 committee.
 Member of the Executive Committee of the ACM Special Interest
Group on Logic and Computation (SIGLOG), starting April 2014.
 Chair of the SIGLOG Executive Committee Nominating Committee,
Fall 2015.
 Program committee cochair for the Joint Meeting of the 23rd
EACSL Annual Conference on Computer Science Logic (CSL14) and the 29th
ACM/IEEE Symposium on Logic in Computer Science (LICS14), July 2014
(Program Committee coChair).
 Expert Panel Member for the midterm evaluation of Linnaeus
Grants for Swedish research centers in the areas of Physical Sciences
and Engineering, January 2014.
 Member of the Steering Committee of Certified
Programs and Proofs (CPP), since 2012.
 Panel member of the 2012 CASC Theorem Proving System
Competition, Mancester, June 2012.
 Member of the FICS Workshop Steering Committee, 20122015.
 Program committee cochair for CPP 2012: Second International
Conference on Certified Programs and Proofs, 1315 December, Kyoto,
Japan.
 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, 20112113.
 Member of the IJCAR (International Joint Conference of
Automated Reasoning) Steering Committee, 20112112.
 Program committee cochair for IJCAR 2012: International Joint
Conference of Automated Reasoning, Manchester, UK, June 2012.
 Program Committee coChair for FICS 2012: Fixed Points in
Computer Science (a satellite workshop of ETAPS 2012), Tallinn,
Estonia.
 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.
 Coorganizer of 2009 Workshop on ProofSearch in Type Theories
(PSTT), 3 August 2009, a CADE 2009 affiliated workshop, Montreal,
Canada.
 Inria Saclay hiring committee for CR2, Spring 2008.
 Program cochair 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, 2529 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), 1415 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, 1213 June 1996, Boston. Sponsored by the NSF and Army
Research Office.
 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

“A special issue on structural proof theory, automated
reasoning and computation in celebration of Dale Miller’s 60th
birthday”, Volume 29, Special Issue 8 of the
journal Mathematical Structures in Computer Science, September
2019, Cambridge University Press.
 LICS TestofTime Award 2014 for a paper appearing in
LICS 1994.
 ERC Advanced Grant titled “ProofCert: Broad Spectrum Proof
Certificates” for 2.2 million euros for the five years 20122016.
 LICS TestofTime Award 2011 for a paper coauthored with Joshua
Hodas in LICS 1991.
 Finalist in the 33^{rd} Westinghouse Science Talent Search
(now the Regeneron Science Talent Search), 1974.
Invited Speaker at Conferences and Workshops
 Seventh Meeting of ANRFWF Project Ticamore (Translating and
dIscovering CAlculi for MOdal and RElated logics), 1617 June 2021.
 TeaseLP 2020 (Trends, Extensions, Applications and
Semantics of Logic Programming), an ETAPS Workshop, 2829 May 2020.
 16th International Conference on Distributed Computing and
Internet Technology (ICDCIT), Kalinga Institute of Industrial
Technology, Bhubaneswar, Odisha, India. 912 January 2020.
 Workshop on Proof Theory for Automated Deduction, Automated
Deduction for Proof Theory, 2325 October 2019, Funchal, Madeira.
 Third Tübingen Conference on ProofTheoretic Semantics, 2730
March 2019.
 Workshop on Proof Theory and its Applications, 67 September
2018 in Ghent, Beligum.
 LAP 2017: Sixth Conference on Logic and Applications, 1822
September 2017, Dubrovnik, Croatia.
 PADL 2017: Nineteenth International Symposium on Practical
Aspects of Declarative Languages, 1617 January 2017, Paris.
 Workshop on linear logic, mathematics and computer science as
part of “LL2016Linear Logic: interaction, proofs and computation”,
710 November 2016, Lyon. France.
 Linearity 2016. Porto, 25 June 2016.
 Research seminar titled “Interactions between logic, computer
science and linguistics: history and philosophy”, Université de
Lille 3, 15 June 2016.
 CIPPMI (Current issues in the philosophy of practice of
mathematics and informatics) Workshop on Proofs, justifications and
certificates. 34 June 2016, Toulouse, France.
 TYPES 2016: 22nd International Conference on Types for Proofs
and Programs. Novi Sad, Serbia, 2326 May 2016.
 LSFA 2015: 10th Conference on Logical and Semantic Frameworks,
with Applications, Natal Brazil, 30 August  1 September 2015.
 Session on History and Philosophy of Computing at
the 15th Congress of Logic, Methodology and Philosophy of Science,
Helsinki, 38 August 2015.
 LOPSTR 2015: 25th International Symposium on LogicBased Program
Synthesis and Transformation and PPDP 2015: 17th International Symposium on
Principles and Practice of Declarative Programming, Siena, 1316 July 2015.
 ∀ X.XΠ 2014: All about Proofs, Proofs for All, part of
the Vienna Summer of Logic, 18 July 2014.
 LATD 2014: Logic, Algebra, and Truth Degrees, part of the Vienna
Summer of Logic, 1619 July 2014.
 LFMTP 2013: Logical Frameworks and MetaLanguages: Theory and
Practice, affiliated with ICFP’13, Boston, 23 September 2013.
 ANRDFG Hypothese Workshop titled Different Aspects of
Proof Theory, ENS Paris, 3 May 2012.
 Journees nationales du GDRIM, 2526 January 2012,
University of Paris 7.
 LMPS 2011: 14th International Congress of Logic, Methodology and
Philosophy of Science, Nancy, France, 1926 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, 2122 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, 2829 September 2009.
 LAM 2009: Logics for Agents and Mobility. A workshop associated
to LICS09. 910 August 2009.
 Journées du projet PEPSRelations, 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, 34 July 2008.
 LFMTP 2008: International Workshop on Logical
Frameworks and MetaLanguages: 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, 2425 October
2007, Vienna, Austria.
 IJCAR 2006: Joint Conference on Automated Reasoning (part of
FLoC 2006). Seattle, 1621 August 2006.
 Geometria della Logica, Facoltà di Lettere e Filosofia,
Università di Roma Tre, 2829 April 2006.
 Algebraic Process Calculus: The first 25 years and beyond,
Bertinoro, Italy, 5 August 2005.
 Structure and Deduction 2005: an ICALP workshop, Lisbon, 1617
July 2005.
 2nd TaiwaneseFrench Conference in Information Technologies,
Tainan, Taiwan, 2325 March 2005.
 CSL 2004: 13th Annual Conference of the European Association for
Computer Science Logic, Karkonoski National Park, Poland, 2023
September 2004.
 TPHOLs 2003: International Conference on Theorem Proving in
Higher Order Logics, 912 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,
89 June 2003, Valencia, Spain.
 FSTTCS02: 22nd Foundations of Software Technology and
Theoretical Computer Science, 1214 December 2002, Indian Institute of
Technology, Kanpur, India.
 AMAST02: 9th International Conference on Algebraic Methodology
And Software Technology, September 913, 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, 1012 July 2000, University of East
Anglia, Norwich, U.K.
 European Meeting of the Association for Symbolic Logic,
Utrecht, 16 August 1999.
 TYPES’96: Workshop on Types, Aussois, France, 1619 December 1996.
 Conference on Logical Aspects of Computational Linguistics,
Nancy, 2325 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.
 GULPPRODE’95: ItalianSpanish 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 CompulogNetwork 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 “HigherOrders”, 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
TypeTheory, Ohio State Univ, 8 April 1984.
Invited Tutorials and Advanced Courses

Graduate level course on “The proof theoretic foundation of
computational logic,” Dipartimento di Informatica, Università
di Pisa, 1016 September 2014.
 CUSO Winter School in Mathematics and Computer Science “Proof
and Computation”, Les Diablerets, Switzerland, 2731 January 2013.
 Graduate level course on “Proof theory with applications to
computation and deduction,” Dipartimento di Informatica, Università
di Pisa, 1930 September 2011.
 PLS8: 8th Panhellenic Logic Symposium, Ioannina, Greece, July
48, 2011. Three hour tutorial.
 ISCL: International School on Computational Logic, Bertinoro,
1015 April 2011. Six hours of lectures.
 Graduate level course on “Proof search and Computation.”
Dipartimento di Scienze dell’Informazione, Universitá degli studi di
Milano, 1526 March 2010.
 Graduate level course on “Proof systems for linear,
intuitionistic, and classical logic.” Dipartimento di Informatica,
Universitá Ca’ Foscari di Venezia, 1524 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 ProofsasPrograms 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, 314 June 2002.
 International School on Computational Logic (ISCL), Acquafredda
di Maratea (Basilicata, Italy), September 49, 2000. Sponsored by
Association for Logic Programming (ALP), the European COMPULOG net and
by GULP.
 Eleventh European Summer School in Logic, Language and
Information (ESSLLI99), August 1999, Utrecht.
Cotaught 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

2021

Online Worldwide Seminar on Logic and Semantics (OWLS), 10 March
• Proof Theory Virtual Seminar, 3 March.
 2019

University of Minnesota, 19 June
• Australian National University, 1 May and 8 May.
 2018

Technical University of Vienna, 31 October
• Cyber Security Lab, NTU, Singapore, 21 March.
 2017

SD 2017: Structures and Deduction, Oxford, UK, 8 September
• TLLA 17: Trends in Linear Logic and Applications, 3 September
• Sémin’ouvert du LIX, 23 February
 2016

ACADIA research centre, Ca’ Foscari University, Venice, 27 April
 2015

Journées ANR Rapido, PPS, 18 June
• Semantics and Verification group at PPS, 11 June
• ETH Zurick Department of Computer Science Distinguished Colloquium Series, 20 April
• Inria Paris, Deducteam Seminar, 30 January
 2014

IT University of Copenhagen, 11 September
 2013

Groupe de travail Sémantique, PPS, University of Paris
Diderot, 4 June
• College of Engineering & Computer Science, Australian National
University, 14 May
• Department of Mathematics and Computer Science, Freie
Universität Berlin, 22 February.
 2012

Pisa Summer Workshop on Proof Theory. 1215 June
• CHocCoLa seminar, ENS Lyon, 15 March
• Workshop on Certificates and Computation, ITU Copenhagen, 12 March
• Department of Mathematics, Carnegie Mellon University, 5 April.
 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
• Chalmers University of Technology, Göteborg, Sweden, 2324 May
• Technical University of Vienna, 12 January.
 2010

University of Minnesota, 10 November
• University of Bath, 15 September
• INRIALoria, Nancy, 12 March
• LRI, University of Paris South, 8 October.
 2008
 Laboratoire "Preuves, programmes, systémes" (PPS), 13 Nov
• Workshop on Proofsearch in Type Theories, LIX, 5 June.
 2007
 ICMS Workshop on Mathematical Theories of Abstraction,
Substitution and Naming in Computer Science, Edinburgh, UK, 2529 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 TaiwaneseFrench Conference in Information Technologies,
Tainan, Taiwan, 2325 March.
 2004
 INRIALoria, 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, CNRSUniversité de Paris Sud, 30 January.
 2003
 Groupe de travail "Sémantique", PPS Paris VII, 2 December
• Workshop PCRICEA 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 NotreDame
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, CNRSUniversité de Paris Sud, 19 November.
• Departamento de Informatica, Pontificia Universidade Catolica do
Rio de Janeiro (PUCRio), 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.
• MidAtlantic Logic Conference, Philadelphia, PA, 17 February.
 1984

HewlettPackard, Palo Alto, CA, 23 January.
Conference and Workshop Program Committees
 2022
 CiE 2022: Computability in Europe 2022, Swansea, UK, July 2022.
 2021
 RAMiCS 2021: 19th International Conference on Relational and Algebraic
Methods in Computer Science, CIRM, Luminy, France, 25 November.
• LPAR23: 23rd International Conference on Logic for Programming,
Artificial Intelligence and Reasoning, online, 1213 January.
 2020
 WFLP 2020: 28th International Workshop on Functional and
Logic Programming, Bologna, Italy, 7  10 September.
• IJCAR2020: 10th International Joint Conference on
Automated Reasoning, Paris, 29 June  2 July 2020.
• TEASELP: Workshop on Trends, Extensions, Applications and
Semantics of Logic Programming, Dublin, 25 April (associated
with ETAPS).
 2019

TABLEAUX 2019: Automated Reasoning with Analytic Tableaux and
Related Methods, London, 35 September.
• LFMTP’19: Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, 22 June, Vancouver, Canada (Program
Committee coChair).
 2018
 IJCAR2018: 9th International Joint Conference on
Automated Reasoning, Oxford, 1417 July 2018.
 2017
 FSCD’17: Second International Conference on Formal
Structures for Computation and Deduction, Oxford, 36 September
(Program Committee Chair).
• 26th International Conference on Automated Deduction,
Gothenburg, Sweden, 611 August.
 2016
 FSCD’16: First International Conference on Formal
Structures for Computation and Deduction, Porto, Portugal, 2226
June.
• IJCAR 2016: International Joint Conference on Automated
Reasoning, Ciombra, Portugal, 27 June  2 July.
• CPP 2016, Fifth International Conference on Certified Programs
and Proofs, 1819 January, Saint Petersburg, Florida.
 2015

TABLEAUX 2015: Automated Reasoning with Analytic Tableaux and
Related Methods, Wroclaw, Poland, September.
• PPDP 2015: 17th International Symposium on Principles and
Practice of Declarative Programming, Siena, Italy, 1316 July.
• PxTP 2015: Fourth Workshop on Proof eXchange for Theorem
Proving, Berlin, Germany, 23 August.
• ICALP 2015 (42nd International Colloquium on Automata, Languages,
and Programming), Track B, Kyoto, Japan, 610 July.
 2014

WoLLIC 2014: Workshop on Logic, Language, Information and
Computation, Valparaiso Chile, 14 September.
• Joint Meeting of the 23rd EACSL Annual Conference on Computer
Science Logic (CSL14) and the 29th ACM/IEEE Symposium on Logic
in Computer Science (LICS14), 1418 July (Program Committee
coChair).
 2013

Tableaux 2013, 1619 September, Nancy, France.
 2012

CPP 2012: Second International Conference on Certified Programs
and Proofs, 1315 December, Kyoto, Japan (Program Committee coChair).
• LFMTP’12: Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, 9 September, Copenhagen, Denmark.
• LAM 2012: Fifth International Workshop on Logics, Agents, and
Mobility, June, Hamburg, Germany.
• LPAR18: The 18th International Conference on Logic for
Programming, Artificial Intelligence and Reasoning. Merida,
Venezuela, 1115 March.
• FICS 2012: Fixed Points in Computer Science (a satellite
workshop of ETAPS 2012), Tallinn, Estonia, 24 March (Program Committee
coChair).
• IJCAR 2012: International Joint Conference on Automated
Reasoning, Manchester, UK, June (Program Committee coChair).
 2011

LAM 2011: Fourth International Workshop on Logics, Agents, and
Mobility, 10 September, Aachen, Germany.
• MLPA11: Modules and Libraries for Proof Assistants, 26 August,
Nijmegen.
• LICS 2011: Logic in Computer Science, 2124 June, Toronto.
• Tableaux 2011: 20th International Conference on Automated
Reasoning with Analytic Tableaux and Related Methods, July 48,
Bern, Switzerland.
 2010

LPAR17: 17th International Conference on Logic for Programming
Artificial Intelligence and Reasoning, Yogyakarta, Indonesia,
1115 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 ProofSearch in Type Theories, FLoC 2010,
Edinburgh, 15 July.
• Workshop on Programming Languages for Mechanized
Mathematics Systems (PLMMS), 5 July.
• IFIPTCS 2010: International Conference on Theoretical Computer
Science, part of the World Computer Congress in Brisbane, 2023
September.
 2009

Workshop on Games, Dialogue and Interaction, 2829 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, 711 September, Coimbra, Portugal.
• LSFA 2009: Fourth Logical and Semantic Frameworks, with
Applications, part of RDP 2009, 28 June3 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,
1517 July.
• ESHOL 2008: Evaluation of Systems for Higher Order Logic, part
of IJCAR 2008, Sydney, Australia, 1015 August.
• LAM 2008: Logics for Agents and Mobility Workshop, part of
ESSLLI 2008, Hamburg, Germany, 415 August.
• LSFA08: Third Workshop on Logical and Semantic Frameworks with
Applications, Brazil.
• CSL08: 17th Annual Conference of the European Association for Computer
Science Logic, 1520 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, 1416 April, Ise, Japan.
 2007

LFMTP’07: Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, August, Bremem, Germany.
• WoLLIC’07: Fourteenth Workshop on Logic, Language, Information
and Computation, Rio de Janeiro, 25 July.
• CADE21: 21st Conference on Automated Deduction, 17  20 July
Bremen, Germany.
 2006

FSTTCS’06: Foundations of Software Technology and Theoretical
Computer Science, Kolkata, India. 1315 December.
• LPAR13: 13th International Conference on Logic for Programming
Artificial Intelligence and Reasoning, Phnom Penh, Cambodia.
1317 November.
• LFMTP’06: Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, 16 August.
• TFIT’06: TaiwaneseFrench Conference on
Information Technology, Nancy, France. 2830 March.
• Geocal Workshop on Logic Programming and Concurrency, 27 February  3
March, CIRM, Luminy, France (Program Committee coChair)
 2005

MoVeLog’05: A Workshop on Mobile Code Safety and Program Verification
Using Computational Logic Tools. Barcelona, Spain, 5 October.
• LPAR11: 11th International Conference on Logic for Programming,
Artificial Intelligence, and Reasoning. Montevideo, Uruguay,
1418 March
• CSL05: 14th Annual Conference of the European Association for Computer
Science Logic, 2225 August, Oxford, UK
• CADE20: Conference on Automated Deduction, Tallinn, Estonia,
2227 July.
 2004

ICLP’04: Twentieth International Conference on Logic
Programming, SaintMalo, France, 69 September.
• LFM04: Fourth International Workshop on Logical Frameworks and
MetaLanguages.
 2003

ACMSigplan 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, 1214 July, Budapest, Hungary.
• LPAR 2003: 10th International Conference on Logic for
Programming Artificial Intelligence and Reasoning, 2226 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, PUCRio,
Rio de Janeiro, 57 June.
• PPDP02: International Conference on Principles and Practice of
Declarative Programming. Pittsburgh, 68 October 2002.
• CSL02: 11th Annual Conference of the European Association for Computer
Science Logic, 2225 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 Metalanguages.
 2001

Dagstuhl Seminar on Proof Theory in Computer Science (01411),
October 712.
• ICoS3: Inference in Computational Semantics, 1819 June.
• FLOPS 2001: 5th International Symposium on Functional and
Logic Programming, Waseda University, Tokyo, 79 March.
 2000

CONCUR2000: 11th International Conference on Concurrency Theory,
August 2225, Pennsylvania State University. Conference coOrganizer
and PC member.
• ICoS2: Inference in Computational Semantics, Dagstuhl,
Germany, 2930 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 ComponentBased 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, 812 July.
• CATS 97: Computing: The Australasian Theory Symposium, Sydney,
Australia, 37 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 Metaprogramming 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 Metaprogramming and
Logic, April, Leuven, Belgium.
 1989

ICLP89: Sixth International Conference on Logic Programming,
August, Lisbon Portugal.
External Examiner

External Examiner for PhDs after 2010:
Ahmed Bhayat, University of Manchester, 6 January 2021 (reporter).
• Aurore Alcolei, ENS Lyon, 17 October 2019 (rapporteur).
• Michael Lettmann, Technical University of Vienna, 30 October 2018
(reporter).
• Raphaël Cauderlier, CNAM, 10 October 2016 (rapporteur).
• Gabriel Scherer, University of Paris Diderot, 30 March 2016 (rapporteur).
• Ali Assaf, École Polytechnique, 28 September 2015 (president).
• Taus BrockNannestad, IT University of Copenhagen, 12 September
2014 (reporter).
• Thanos Tsouanas, ENS Lyon, 2 July 2014 (rapporteur).
• Mahfuza Farooque, École Polytechnique 19 December 2013.
• Stéphane Zimmermann, University of Paris Diderot, 10 December
2013 (president).
• Matthias Puech, University of Bologna, 8 April 2013 (rapporteur).
• Robert Simmons, Carnegie Mellon University, 22 October 2012.
• Nicolas Pouillard, University of Paris 7, 13 January 2012 (rapporteur).
• Anders Starcke Henriksen, University of Copenhagen, December 2011 (reporter).
• Francois Garillot, École Polytechnique, 5 December 2011 (president).
• Daniel Weller, Technische Universität Wien, 12 January 2011 (reporter).
 External Examiner for PhDs during 20002010:
• Elie Soubiran, École Polytechnique 27 September 2010 (president).
• Clement Houtmann, Nancy, 12 March 2010 (examinateur).
• Denis Cousineau, École 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, École polytechnique, 6 May 2004 (examinateur).
• Sorin Craciunescu, École polytechnique, March 2004 (rapporteur).
• Kumar Neeraj Verma, LSV, ENSCachan, September 2003
(examinateur).
• Kai Brünnler, Department of Computer Science, TU Dresden,
September 2003.
• Veronique Cortier, LSV, ENSCachan, 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 HuiBonHoa, 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.
• JeanMarc 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:
Olivier Hermant, 20 April 2017 (reporter)
• Stefan Hetzl, 5 November 2012 (reporter)
• Frédéric Blanqui, 13 July 2012 (examiner and president)
• Agata Ciabattoni, March 2007 (reporter)
• Gilles Barthe, June 2004 (examiner)
• Delia Kesner, Nov 2001 (reporter)
• JeanMarc Andreoli, May 2001 (reporter)
 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, EPSRC, UK.
Ph.D. Dissertation Supervision

In progress: Matteo Manighetti and Emily Grienenberger (jointly
supervised with Gilles Dowek).
 Ulysse Gérard, “Computing with relations, functions, and
bindings”, 18 October 2019, Ecole Doctorale de l’Institut
Polytechnique de Paris.
 Sonia Marin, “Modal proof theory through a focused telescope”,
30 January 2018, University of ParisSaclay (coadvised with
L. Straßburger).
 Roberto Blanco, “Applications for Foundational Proof
Certificates in theorem proving”, 21 December 2017, University of
ParisSaclay.
 Zakaria Chihani, “Certification of firstorder proofs in classical and
intuitionistic logics”, 2 November 2015, Ecole Polytechnique.
 Ivan Gazeau, “Safe Programming in Finite Precision: Controlling
Errors and Information Leaks”, 14 October 2013, Ecole Polytechnique
(coadvised with C. Palamidessi).
 Olivier Delande, “Symmetric Dialogue Games in the Proof Theory
of Linear Logic,” 15 October 2009, Ecole Polytechnique.
 Vivek Nigam, “Exploiting noncanonicity in the sequent
calculus,” 18 September 2009, Ecole Polytechnique. Fellow of the
Alexander von Humboldt Scholarship.
 David Baelde, “A linear approach to the prooftheory 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. Coadvised with Carlos
Camarão de Figueiredo.
 Ray McDowell, “Reasoning in a Logic with Definitions and Induction,”
September 1997, University of Pennsylvania.
 Chuck Liang, “Objectlanguage substitution and unification in
metalogic,” 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, “Prooftheoretic methods for analysis of
functional programs,” August 1990, University of Pennsylvania.
 Amy Felty, “Implementing theorem provers in a higherorder logic
programming language,” August 1989, University of Pennsylvania.
 Gopalan Nadathur, “A higherorder 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, “ObjectOriented 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.
Supervised Post Docs and Staff

Noam Zeilberger, post doc ProofCert, from Oct 2015.
 Hugh Steele, post doc ProofCert, from 1 Dec 2015.
 Matthias Puech, post doc ProofCert, from Oct 2015.
 Tomer Libal, engineer ProofCert, from Jan 2015.
 Giselle Reis, post doc ProofCert, from Nov 2014 to Jul 2016.
 Marco Volpe, post doc ProofCert, from Nov 2014.
 Taus BrockNannestad, post doc ProofCert, from Oct 2014.
 Danko Ilik, post doc ProofCert, from Dec 2013.
 Matteo Cimini, post doc Inria, from Oct 2012 to Jan 2014.
 Fabien Renaud, post doc ProofCert, from Sep 2012 to Aug 2013.
 Quentin Heath, junior engineer at Inria, from Sep 2011 to Aug 2013.
 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 2007.
 Murdoch Gabbay, post doc at Inria, from July 2003 to July 2004.
 Kamal AboulHosn, 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.
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 tenweek 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 HuiBonHoa, 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.
 JeanYves Girard, October – November 1987.
Professor from the University Paris VI.
Publications
Books
 Programming with higherorder logic, with Gopalan
Nadathur, Cambridge University Press. June 2012. ISBN: 9780521879408.
Refereed Journal Publications
 “The undecidability of proof search when equality is a logical
connective” with Alexandre Viel. To appear in the Special
Issue on Theoretical and Practical Aspects of Unification in
the Annals of Mathematics and Artificial Intelligence.
 “Reciprocal influences between proof theory and logic
programming”. Philosophy & Technology, 34(1), 75104 (2021).
First appeared online August 2019.
 “A Proof Theory for Model Checking” with Quentin Heath.
Journal of Automated Reasoning, 63(4), 857885.
First appeared online June 2018.
 “Mechanized metatheory revisited”. Journal of Automated
Reasoning, 63(3), pp. 625665 (October 2019). First appeared online
October 2018.
 “Proof checking and logic programming”. Formal Aspects
of Computing, 29(3), 383399 (May 2017).
 “A semantic framework for proof evidence” with Zakaria Chihani
and Fabien Renaud. Journal of Automated Reasoning 59(3):
287330 (2017).
 “A multifocused proof system isomorphic to expansion proofs”
with Kaustuv Chaudhuri and Stefan Hetzl. A special issue of the J. of Logic and Computation in honor of Roy Dyckhoff, 26(2): 577603 (2016).
 “Preserving differential privacy under finiteprecision
semantics” with Ivan Gazeau and C. Palamidessi. TCS 655: 92108
(2016).
 “Abella: A System for Reasoning about Relational
Specifications” with David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Gopalan
Nadathur, Alwen Tiu, and Yuting Wang. J. of Formalized
Reasoning, 7(2), pp. 189 (2014).
 “A formal framework for specifying sequent calculus proof
systems” with Elaine Pimentel. Theoretical Computer
Science, Vol. 474, pp. 98–116 (2013).
 “Kripke Semantics and Proof Systems for Combining
Intuitionistic Logic and Classical Logic” with Chuck Liang.
Annals of Pure and Applied Logic, 164(2), pp. 86111, February
2013.
 “A twolevel logic approach to reasoning about
computations” with Andrew Gacek and Gopalan Nadathur. Journal
of Automated Reasoning, 49(2) (2012), pp. 241273.
 “A Focused Approach to Combining Logics” with
Chuck Liang. Annals of Pure and Applied Logic, 162 (2011), pp.
679697.
 “Nominal abstraction” with Andrew Gacek and Gopalan Nadathur.
Information & Computation, 209, 2011, pp. 4873.
 “A framework for proof systems,” with Vivek Nigam. Journal of Automated Reasoning, 45(2), 2010, pp. 157188.
 “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. 654672.
 “Focusing and Polarization in Linear, Intuitionistic, and
Classical Logics,” with Chuck Liang. Theoretical Computer
Science, 410(46), 2009, pp. 47474768.
 “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. 411437 (2003).
 “Reasoning with HigherOrder Abstract Syntax in a Logical
Framework” with Raymond McDowell. ACM Transactions on
Computational Logic, Vol. 3(1), 80136 (2002).
 “CutElimination 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 MarchettiSpaccamela, and
Peter Wegner.
 “Logical Foundations for Open System Design,” Computing
Surveys 28(4): 48 (1996).
 “Forum: A multipleconclusion specification logic”.
Theoretical Computer Science, 165(1): 201232 (1996).
 “Logic programming in a fragment of intuitionistic linear
logic,” with Joshua Hodas. Information and
Computation, 110(2), 327365 (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 lambdaabstraction, 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).
 “Higherorder 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
 “Two applications of logic programming to Coq”, with Matteo
Manighetti and Alberto Momigliano. PostProceedings for TYPES 2020,
LIPIcs, Volume 188 (March 2021).
 “Extrinsically Typed Operational Semantics for Functional
Languages”, with Matteo Cimini and Jeremy Siek. Proceedings of the
ACM SIGPLAN International Conference on Software Language Engineering
(SLE), 1520 November 2020.
 “A distributed and trusted web of formal proofs”.
Proceedings of the 16th International Conference on Distributed
Computing and Internet Technology (ICDCIT 2020), 912 January 2020,
Kalinga Institute of Industrial Technology, Bhubaneswar, Odisha,
India. Invited paper.
 “Functional programming with λtree syntax”, with
Ulysse Gérard and Gabriel Scherer. Proceedings
of PPDP 2019: International Conference on Principles and Practice of
Declarative Programming, edited by E. Komendantskaya, October 2019.
 “PropertyBased Testing via Proof Reconstruction”, with
Roberto Blanco and Alberto Momigliano. Proceedings
of PPDP 2019: International Conference on Principles and Practice of
Declarative Programming, edited by E. Komendantskaya, October 2019.
 “A ProofTheoretic Approach to Certifying Skolemization”, with
Kaustuv Chaudhuri and Matteo Manighetti. Proceedings of the 8th ACM
SIGPLAN International Conference on Certified Programs and Proofs (CPP’19),
pages 7890, January 2019.
 “Mechanized Metatheory Revisited: An Extended Abstract”.
Post proceedings of the 22nd International Conference on Types for
Proofs and Programs (TYPES 2016), edited by S. Ghilezan,
H. Geuvers, and J. Ivetić. Leibniz International Proceedings in
Informatics (LIPIcs) Volume 97, 2018, pp. 1:1–1:16,
 “Computationasdeduction in Abella: work in progress” with
Kaustuv Chaudhuri and Ulysse Gérard. Proceedings of LFMTP 2018:
Logical Frameworks and MetaLanguages: Theory and Practice, Oxford,
7 July 2018.
 “Influences between logic programming and proof theory”.
HaPoP 2018: Fourth Symposium on the History and
Philosophy of Programming, Oxford, 22 March 2018.
 “Using linear logic and proof theory to unify computational
logic”. Proceedings of TLLA 2017: Trends in Linear Logic and
Applications. Oxford, 3 September 2017.
 “Separating Functional Computation from Relations” with Ulysse
Gérard. Proceedings of CSL 2017. Stockholm, Sweden, 2017.
 “Translating between implicit and explicit versions of proof”
with Roberto Blanco and Zak Chihani. Proceedings of CADE26, 255273.
Gothenburg, Sweden, 2017.
 “A focused framework for emulating modal proof systems” with
Sonia Marin and Marco Volpe. Proceedings of AiML 2016: Advances in
Modal Logic. Budapest, 2016.
 “Proof Certificates for Equality Reasoning” with Zakaria
Chihani. Postproceedings of LSFA 2015: 10th Workshop on Logical and
Semantic Frameworks, with Applications. Natal, Brazil. ENTCS 322,
pp. 93108. 2016.
 “Functionsasconstructors Higherorder Unification” with
Tomer Libal. Proceedings of Formal Structures for Computation and
Deduction 2016. LIPIcs Volume 52, 26:1–26:17.
 “Proof Outlines as Proof Certificates: a system description”
with Roberto Blanco. Proceedings of the First International Workshop on
Focusing, 23 November 2015, Suva, Fiji. EPTCS Volume 197.
 “On Subexponentials, Synthetic Connectives, and MultiLevel
Delimited Control” with Chuck Liang.
Proceedings of LPAR20: International Conference on Logic for
Programming, Artificial Intelligence, and Reasoning, Nov 2015, Fiji.
 “Focused labeled proof systems for modal logic” with Marco Volpe.
Proceedings of LPAR20: International Conference
on Logic for Programming, Artificial Intelligence, and Reasoning, Nov
2015, Fiji.
 “A framework for proof certificates in finite state
exploration” with Quentin Heath. In the Proceedings of
PxTP 2015: the Fourth Workshop on Proof eXchange for Theorem Proving,
pp. 1126.
 “Proof Checking and Logic Programming” by Dale Miller.
Invited talk. In the Proceedings of PPDP 2015: International
Conference on Principles and Practice of Declarative Programming,
edited by Elvira Albert, p. 18.
 “Foundational Proof Certificates”. In the Proceedings of
APPA2014: All about Proofs, Proofs for All, edited by D. Delahaye and
B. Woltzenlogel Paleo, pp. 150163 (College Publications, 2015).
 “A lightweight formalization of the metatheory of
bisimulationupto” with Kaustuv Chaudhuri and Matteo Cimini.
Proceedings of CPP 2015: The 4th ACMSIGPLAN Conference on Certified
Programs and Proofs. Mumbai, India, January 13  14, 2015, pp.
157166.
 “Communicating and trusting proofs: The case for foundational
proof certificates.” Proceedings of the 14th
Congress of Logic, Methodology and Philosophy of Science in Nancy,
France, 1926 July 2011. Edited by P. SchroederHeister, W. Hodges,
G. Heinzmann, and P. E. Bour, pp. 323342. Published by College
Publications, 2014.
 “Extracting Proofs from Tabled Proof Search” with Alwen Tui.
CPP 2013: Certified Programs and Proofs, Springer LNCS 8307, pp.
194–210, December 2013.
 “Unifying Classical and Intuitionistic Logics for Computational
Control” with Chuck Liang. Proceedings of LICS 2013: 28th Symp. on
Logic in Computer Science.
 “Checking foundational proof certificates for firstorder logic
(extended abstract)” with Zakaria Chihani and Fabien Renaud. PxTP
2014: Workshop on Proof Exchange for Theorem Proving, 910 June
2013, Lake Placid, USA.
 “Foundational proof certificates in firstorder logic” with
Zakaria Chihani and Fabien Renaud. CADE 24: Conference on Automated
Deduction, Ed. M. P. Bonacina. Springer LNAI 7898, pp. 162–177.
 “A Systematic Approach to Canonicity in the Classical Sequent
Calculus” with Kaustuv Chaudhuri and Stefan Hetzl. CSL 2012:
Computer Science Logic, 36 September 2012, Fontainebleau, France.
 “A nonlocal method for robustness analysis of floating point
programs” with Ivan Gazeau and Catuscia Palamidessi.
QAPL 2012: Tenth Workshop on Quantitative Aspects of Programming
Languages, 31 March  1 April 2012, Tallinn, Estonia. EPTCS 85, pp.
63–76.
 “A proposal for broad spectrum proof certificates.”
CPP 2011: First International Conference on Certified
Proofs and Programs, 79 December 2011, Taiwan, December 2011. LNCS
7086, pp. 5469.
 “Reasoning about computations using twolevels 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. 3446.
 “Focused inductive theorem proving,” with David Baelde and
Zachary Snow. IJCAR: International Joint Conference on Automated
Reasoning, July 2010, Edinburgh. LNCS 6173, pp. 278292.
 “Finding Unity in Computational Logic.” ACMBCS Visions of
Computer Science 2010 conference, 1316 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, 79 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, 1114 August 2009.
 “Reasoning in Abella about Structural Operational Semantics
Specifications,” with Andrew Gacek and Gopalan Nadathur. LFMTP 2008:
International Workshop on Logical Frameworks and MetaLanguages:
Theory and Practice, Pittsburgh, June 2008, pp. 75–89.
 “Canonical Sequent Proofs via MultiFocusing,” with Kaustuv
Chaudhuri and Alexis Saurin. Proceedings of the IFIP International
Conference on Theoretical Computer Science, September 2008, pp.
383–396.
 “Focusing in linear metalogic,” 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. 92106.
 “Focusing and Polarization in Intuitionistic Logic”
with Chuck Liang. CSL07: Computer Science Logic 2007. LNCS 4646,
pp. 451465.
 “Incorporating tables into proofs” with Vivek
Nigam. CSL07: Computer Science Logic 2007. LNCS 4646,
pp. 466480.
 “From proofs to focused proofs: a modular proof of focalization in
Linear Logic” with Alexis Saurin. CSL07: Computer Science Logic 2007. LNCS 4646,
pp. 405419.
 “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, 391397.
 “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 ACMSIGPLAN International Symposium on Principles and
Practice of Declarative Programming (PPDP’06), Venice, Italy, 1012
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 HigherOrder
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 namepassing 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, 111135 (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. 118127.
 “Encryption as an Abstract DataType: An extended abstract,”
Proceedings of FCS’03: Foundations of Computer Security, edited by
Iliano Cervesato, pp. 314, 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.
 “Higherorder quantification and proof search.” Proceedings
of AMAST 2002, LNCS 2422, edited by Hélène Kirchner and Christophe
Ringeissen. pp. 6074.
 “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.
Electronic Notes of TCS, 58(1), edited by R. L. Crole, S. J. Ambler,
and A. Momigliano.
 “Abstract Syntax for Variable Binders: An Overview.”
Proceedings of Computational Logic  CL2000, pp. 239253, July 2000,
edited by John Lloyd, et. al. SpringerVerlag, LNAI 1861.
 “A Logic for Reasoning with HigherOrder 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.
Electronic Notices of Theoretical Computer Science, Volume 3.
 “A MultipleConclusion MetaLogic.” Proc. of the 1994
Symposium on Logics in Computer Science, Paris, 272 – 281.
Awarded the TestofTime Award during LICS 2014.
 “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. SpringerVerlag, 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 TestofTime Award during LICS 2011.
 “Unification of Simply Typed LambdaTerms 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 DependentType λCalculus in a Logic
Programming Language” with Amy Felty, the 1990 Conference on
Automated Deduction, SpringerVerlag Lecture Notes in Artificial
Intelligence, Volume 449, edited by Mark Stickel, 221–235.
 “A Logic Programming Language with LambdaAbstraction, Function
Variables, and Simple Unification” in Extensions of Logic
Programming ed. Peter SchroederHeister, SpringerVerlag, 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 higherorder 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 higherorder 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 CoChairs Tom Kehler
and Stan Rosenschein, 198 – 202.
 “Higherorder 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 higherorder 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,
SpringerVerlag, 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, SpringerVerlag, 1982,
50 – 69.
Edited Volumes
 Special Issue of Logical Methods in Computer Science of
Selected Papers of the 2nd International Conference on Formal
Structures and Deduction (FSCD 2017), edited by Ugo Dal Lago and Dale
Miller.
 Proc. of the Fourteenth Workshop on Logical Frameworks and
MetaLanguages: Theory and Practice, LFMTP 2019, 22 June 2019,
Vancouver, Canada. Edited by Dale Miller and Ivan Scagnetto.
Published by EPTCS. DOI 10.4204/EPTCS.307.
 Proc. of the 2nd International Conference on Formal Structures
for Computation and Deduction, FSCD 2017, 29 September 2017, Oxford,
UK. Edited by Dale Miller. Published by LIPIcs. ISBN
9783959770477. DOI 10.4230/LIPIcs.FSCD.2017.0.
 Proc. of the Joint Meeting of the TwentyThird EACSL Annual
Conference on Computer Science Logic (CSL) and the TwentyNinth Annual
ACM/IEEE Symposium on Logic in Computer Science (LICS), CSLLICS 2014,
1418 July 2014, Vienna, Austria. Edited by Thomas Henzinger and Dale
Miller. Published by the ACM. ISBN 9781450328869.
 Proc. of the 2nd International Conference on Certified Programs
and Proofs, CPP 2012, 1315 December, Kyoto, Japan. Edited by Chris
Hawblitzel and Dale Miller. Published by Springer as LNCS 7679.
 Automated Reasoning: 6th International Joint Conference, IJCAR
2012, Manchester, UK, June 2012, Proceedings. Edited by Bernhard
Gramlich, Dale Miller, and Uli Sattler. Published by Springer as LNAI
7364.
 Proc. of the 8th Workshop on Fixed Points in Computer Science,
FICS 2012. Edited by Dale Miller and Zoltán Ésik. Published as
EPTCS 77, Feb 2012.
 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 2629, 1993. MIT Press 1993, ISBN 0262631520.
 Proc. of the Workshop on Linear Logic and Logic Programming,
Washington, DC, November 1992. Edited by Dale Miller. Available as
UPenn CIS technical report MSCIS9280.
 Proc. of the Workshop on the λProlog Programming
Language, University of Pennsylvania, July 1992. Edited by Dale
Miller. Available as UPenn CIS technical report MSCIS9286.
Book Chapters
 “Focusing Gentzen’s LK proof system” with Chuck Liang.
Accepted for publication in the volume Peter SchroederHeister
on ProofTheoretic Semantics within the Springer Outstanding
Contributions to Logic.
 “Automation of HigherOrder Logic” with Christoph Benzmüller.
The Handbook of the History of Logic, Volume
9: Logic and Computation, edited by D. Gabbay, J. Siekmann, and
J. Woods (NorthHolland), 2014, pp. 215254.
 “A ProofTheoretic 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 Benzmüller, 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, JeanYves
Girard, Paul Ruet, and Phil Scott. Cambridge University Press, London
Mathematical Society Lecture Notes Series, Volume 316 (2004).
 “Sequent Calculus and the Specification of Computation”
in Computational Logic, edited by U. Berger and H. Schwichtenberg.
NATO Advanced Science Institute Series, subseries F: Computer and
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 MetaLogic” in The Logic of
Computation, edited by H. Schwichtenberg. NATO Advanced Science
Institute Series, subseries F: Computer and Systems Sciences,
published by SpringerVerlag, pp. 265 – 308 (1997). Taken from
lectures given at the International Summer School Marktoberdorf on
Logic of Computation, 25 July  6 August 1995.
 “Higherorder 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 MetaLanguage for Functional Programming” with John Hannan,
in MetaProgramming 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.
Papers in Other Proceedings
 “Andre and the early days of Penn’s Logic and Computation
Group,” in Logic, Language, and Security: ScedrovFest65, LNCS
12300, 2020, DOI 10.1007/9783030620776_6.
 “My colleague, wife, and friend” in The Art of
Modelling Computational Systems: A Journey from Logic and Concurrency
to Security and Privacy. Essays Dedicated to Catuscia Palamidessi on
the Occasion of Her 60th Birthday. LNCS 11769, November 2019. DOI
10.1007/9783030311759.
 “Observations about using logic as a specification language,”
invited paper to the 1995 GulpProde 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, SpringerVerlag.
 “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, SpringerVerlag, 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
 Three entries—titled “Expansion Proofs”, “Focused LK”, and
“Focused LJ”—in Towards an Encyclopaedia of Proof Systems,
edited by Bruno Woltzenlogel Paleo, January 2017.
 “Linear Logic” with Roberto DiCosmo. The Stanford
Encyclopedia of Philosophy (Summer 2019), Edward N. Zalta (ed.).
 “Logic, Higherorder,” 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 Advances in Linear Logic, edited by JeanYves
Girard, Yves Lafont, Laurent Regnier. J. of Symbolic Logic, 62 (2)
1997, pages 678680.
 Review of Invariants, composition, and substitution, by
Ekkart Kindler, Acta Inf. 4 (June 1995), 299312.
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.
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).
 “Higherorder 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 higherorder 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, Volume 8, 61 – 64.
 Advance Problem H237, The Fibonacci Quarterly, Volume 12,
No. 3 (Oct. 1974): 309. This problem introduced what is now called
the Millin Series.
Departmental and University Service at Penn State

Promotion and Tenure Committee, CSE, 20012.
 Strategic Committee, CSE, 20012.
 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
students 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 MPRI: Master Parisien de Recherche en Informatique

Master level course MPRI 21 “Logique linéaire et paradigmes
logiques du calcul”, 20052020.
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 2000.
 CSE 428, Programming Language Concepts, Spring 2000, 02.
 CSE 260, Discrete Mathematics for Computer Science, Fall 2000.
 CSE 597a, Program Analysis Seminar, Fall 2000.
 CSE 522, Semantics of Programming Languages, Spring 2000.
 CSE 468, Theory of Automata, Languages, and Computability.
Spring 1999.
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^{A}T_{E}X by
H^{E}V^{E}A.