Dale Miller
Curriculum Vitae

INRIA Saclay - Île-de-France & Laboratoire d’Informatique, LIX
1 rue Honoré d’Estienne d’Orves
LIX, 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

Supported Visiting Positions

Education

Major Research Interests

Personal Information

Invited Speaker at Conferences and Workshops

Invited Tutorials and Advanced Courses

Colloquia and Seminar Talks

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. 12-15 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, 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.

Conference and Workshop Program Committees

2017
FSCD’17: Second International Conference on Formal Structures for Computation and Deduction, Oxford, 3-6 September (Program Committee Chair). • 26th International Conference on Automated Deduction, Gothenburg, Sweden, 6-11 August.
2016
FSCD’16: First International Conference on Formal Structures for Computation and Deduction, Porto, Portugal, 22-26 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, 18-19 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, 13-16 July. • PxTP 2015: Fourth Workshop on Proof eXchange for Theorem Proving, Berlin, Germany, 2-3 August. • ICALP 2015 (42nd International Colloquium on Automata, Languages, and Programming), Track B, Kyoto, Japan, 6-10 July.
2014
WoLLIC 2014: Workshop on Logic, Language, Information and Computation, Valparaiso Chile, 1-4 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), 14-18 July (Program Committee co-Chair).
2013
Tableaux 2013, 16-19 September, Nancy, France.
2012
CPP 2012: Second International Conference on Certified Programs and Proofs, 13-15 December, Kyoto, Japan (Program Committee co-Chair). • LFMTP’12: Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 9 September, Copenhagen, Denmark. • LAM 2012: Fifth International Workshop on Logics, Agents, and Mobility, 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

Professional Duties

Distinctions

External Examiner

Ph.D. Dissertation Supervision

Master’s Thesis Supervision

Supervised Post Docs and Staff

International Visitors Hosted at the Pennsylvania State University

International Visitors Hosted at the Unversity of Pennsylvania


Publications

Books

  1. Programming with higher-order logic, with Gopalan Nadathur, Cambridge University Press. June 2012. ISBN: 9780521879408.

Refereed Journal Publications

  1. “Proof Checking and Logic Programming”. To appear in Formal Aspects of Computing.
  2. “A semantic framework for proof evidence” with Zakaria Chihani and Fabien Renaud. To appear in the Journal of Automated Reasoning.
  3. “A multi-focused 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): 577-603 (2016).
  4. “Preserving differential privacy under finite-precision semantics” with Ivan Gazeau and Catuscia Palamidessi. TCS 655: 92-108 (2016).
  5. “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. 1-89 (2014).
  6. “A formal framework for specifying sequent calculus proof systems” with Elaine Pimentel. Theoretical Computer Science, Vol. 474, pp. 98–116 (2013).
  7. “Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic” with Chuck Liang. Annals of Pure and Applied Logic, 164(2), pp. 86-111, February 2013.
  8. “A two-level logic approach to reasoning about computations” with Andrew Gacek and Gopalan Nadathur. Journal of Automated Reasoning, 49(2) (2012), pp. 241-273.
  9. “A Focused Approach to Combining Logics” with Chuck Liang. Annals of Pure and Applied Logic, 162 (2011), pp. 679-697.
  10. “Nominal abstraction” with Andrew Gacek and Gopalan Nadathur. Information & Computation, 209, 2011, pp. 48-73.
  11. “A framework for proof systems,” with Vivek Nigam. Journal of Automated Reasoning, 45(2), 2010, pp. 157-188.
  12. “Proof Search Specifications of Bisimulation and Modal Logic for the π-calculus”, with Alwen Tiu. ACM Transactions on Computational Logic, 11(2), 2010.
  13. “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.
  14. “Focusing and Polarization in Linear, Intuitionistic, and Classical Logics,” with Chuck Liang. Theoretical Computer Science, 410(46), 2009, pp. 4747-4768.
  15. “A Proof Theory for Generic Judgments,” with Alwen Tiu. ACM Transactions on Computational Logic, 6(4), October 2005, pp. 749–783.
  16. “Encoding Transition Systems in Sequent Calculus,” with Raymond McDowell and Catuscia Palamidessi. Theoretical Computer Science, 294(3), pp. 411-437 (2003).
  17. “Reasoning with Higher-Order Abstract Syntax in a Logical Framework” with Raymond McDowell. ACM Transactions on Computational Logic, Vol. 3(1), 80-136 (2002).
  18. “Cut-Elimination for a Logic with Definitions and Induction,” with Raymond McDowell. Theoretical Computer Science, Vol. 232, pages 91 - 119 (2000).
  19. “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.
  20. “Forum: A multiple-conclusion specification logic”. Theoretical Computer Science, 165(1): 201-232 (1996).
  21. “Logic programming in a fragment of intuitionistic linear logic,” with Joshua Hodas. Information and Computation, 110(2), 327-365 (1994).
  22. “From operational semantics to abstract machines” with John Hannan. Mathematical Structures in Computer Science, 2(4), 415 – 459 (1992).
  23. “Unification under a mixed prefix.” J. of Symbolic Computation, Vol. 14, 321 – 358 (1992).
  24. “A logic programming language with lambda-abstraction, function variables, and simple unification,” J. of Logic and Computation, 1(4), 497 – 536 (1991).
  25. “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).
  26. “Higher-order Horn clauses” with Gopalan Nadathur, J. of the ACM, 37(4), 777 – 814 (1990).
  27. “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)).
  28. “A compact representation of proofs,” Studia Logica, 46(4), 345 – 368 (1987).

Refereed Conference and Workshop Publications

  1. “A focused framework for emulating modal proof systems” with Sonia Marin and Marco Volpe. Proceedings of AiML 2016: Advances in Modal Logic. Budapest, 2016.
  2. “Proof Certificates for Equality Reasoning” with Zakaria Chihani. Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, Brazil. ENTCS 322, pp. 93-108. 2016.
  3. “Functions-as-constructors Higher-order Unification” with Tomer Libal. Proceedings of Formal Structures for Computation and Deduction (FSCD) 2016. To appear.
  4. “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 vol 197.
  5. “On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control” with Chuck Liang. Proceedings of LPAR-20: International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Nov 2015, Fiji.
  6. “Focused labeled proof systems for modal logic” with Marco Volpe. Proceedings of LPAR-20: International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, Nov 2015, Fiji.
  7. “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. 11-26.
  8. “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.
  9. “Foundational Proof Certificates”. In the Proceedings of APPA2014: All about Proofs, Proofs for All, edited by D. Delahaye and B. Woltzenlogel Paleo, pp. 150-163 (College Publications, 2015).
  10. “A lightweight formalization of the metatheory of bisimulation-up-to” with Kaustuv Chaudhuri and Matteo Cimini. Proceedings of CPP 2015: The 4th ACM-SIGPLAN Conference on Certified Programs and Proofs. Mumbai, India, January 13 - 14, 2015, pp. 157-166.
  11. “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, 19-26 July 2011. Edited by P. Schroeder-Heister, W. Hodges, G. Heinzmann, and P. E. Bour, pp. 323-342. Published by College Publications, 2014.
  12. “Extracting Proofs from Tabled Proof Search” with Alwen Tui. CPP 2013: Certified Programs and Proofs, Springer LNCS 8307, pp. 194–210, December 2013.
  13. “Unifying Classical and Intuitionistic Logics for Computational Control” with Chuck Liang. Proceedings of LICS 2013: 28th Symp. on Logic in Computer Science.
  14. “Checking foundational proof certificates for first-order logic (extended abstract)” with Zakaria Chihani and Fabien Renaud. PxTP 2014: Workshop on Proof Exchange for Theorem Proving, 9-10 June 2013, Lake Placid, USA.
  15. “Foundational proof certificates in first-order logic” with Zakaria Chihani and Fabien Renaud. CADE 24: Conference on Automated Deduction, Ed. M. P. Bonacina. Springer LNAI 7898, pp. 162–177.
  16. “A Systematic Approach to Canonicity in the Classical Sequent Calculus” with Kaustuv Chaudhuri and Stefan Hetzl. CSL 2012: Computer Science Logic, 3-6 September 2012, Fontainebleau, France.
  17. “A non-local 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.
  18. “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.
  19. “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.
  20. “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.
  21. “Finding Unity in Computational Logic.” ACM-BCS Visions of Computer Science 2010 conference, 13-16 April 2010.
  22. “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.
  23. “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.
  24. “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.
  25. “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.
  26. “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.
  27. “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.
  28. “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.
  29. “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.
  30. “Focusing and Polarization in Intuitionistic Logic” with Chuck Liang. CSL07: Computer Science Logic 2007. LNCS 4646, pp. 451-465.
  31. “Incorporating tables into proofs” with Vivek Nigam. CSL07: Computer Science Logic 2007. LNCS 4646, pp. 466-480.
  32. “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.
  33. “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.
  34. “Representing and reasoning with operational semantics.” Proceedings of IJCAR’06 (Third International Joint Conference on Automated Reasoning), 17 - 20 August 2006, Seattle.
  35. “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
  36. “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.
  37. “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.
  38. “A congruence format for name-passing calculi,” with Axelle Ziegler and Catuscia Palamidessi. Proceedings of SOS05: Structural Operational Semantics, 2005.
  39. “A game semantics for proof search: Preliminary results,” with Alexis Saurin. Proceedings of Mathematical Foundations of Programming Semantics, 2005.
  40. “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).
  41. “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).
  42. “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.
  43. “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.
  44. “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.
  45. “Higher-order quantification and proof search.” Proceedings of AMAST 2002, LNCS 2422, edited by Hélène Kirchner and Christophe Ringeissen. pp. 60-74.
  46. “Using linear logic to reason about sequent systems,” with Elaine Pimentel. Proceedings of Tableaux 2002, LNCS, edited by Uwe Egly, Christian G. Fermüller.
  47. “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.
  48. “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.
  49. “A Logic for Reasoning with Higher-Order Abstract Syntax,” with Raymond McDowell. Proceedings of 1997 Symposium on Logics in Computer Science, Warsaw, 434 – 445.
  50. “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.
  51. “Logical Foundations for Open System Design,” Computing Surveys 28(4): 48 (1996).
  52. “A Multiple-Conclusion Meta-Logic.” Proc. of the 1994 Symposium on Logics in Computer Science, Paris, 272 – 281. Awarded the Test-of-Time Award during LICS 2014.
  53. “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.
  54. “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 during LICS 2011.
  55. “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.
  56. “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.
  57. “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.
  58. “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.
  59. “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.
  60. “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.
  61. “Lexical Scoping as Universal Quantification” in the Sixth International Logic Programming Conference, eds. G. Levi and M. Martelli, Lisbon, Portugal, June 1989, 268 – 283.
  62. “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.
  63. “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.
  64. “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.
  65. “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.
  66. “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.
  67. “A theory of modules for logic programming,” IEEE Symposium on Logic Programming, Salt Lake City, September 1986, Program Chair Robert M. Keller, 106 – 114.
  68. “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.
  69. “Higher-order logic programming” with Gopalan Nadathur, Proc. of the Third International Logic Programming Conference, edited by Ehud Shapiro, London, June 1986, 448 – 462.
  70. “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.
  71. “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.
  72. “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.


Edited Volumes

  1. Proc. of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), CSL-LICS 2014, 14-18 July 2014, Vienna, Austria. Edited by Thomas Henzinger and Dale Miller. Published by the ACM. ISBN 978-1-4503-2886-9.
  2. Proc. of the 2nd International Conference on Certified Programs and Proofs, CPP 2012, 13-15 December, Kyoto, Japan. Edited by Chris Hawblitzel and Dale Miller. Published by Springer as LNCS 7679.
  3. 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.
  4. 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.
  5. Proc. of the 2003 International Conference on Principles and Practice of Declarative Programming, PPDP 2003. Edited by Dale Miller. Published by the ACM.
  6. 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.
  7. 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.
  8. 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.


Book Chapters

  1. “Automation of Higher-Order 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 (North-Holland), 2014, pp. 215-254.
  2. “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 Benzmüller, Chad E. Brown, Jörg Siekmann, and Richard Statman, Studies in Logic, published by College Publications, December 2008.
  3. “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 (2004).
  4. “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 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.
  5. “Logic Programming and Meta-Logic” in The Logic of Computation, edited by H. Schwichtenberg. NATO Advanced Science Institute Series, sub-series F: Computer and 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.
  6. “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).
  7. “Abstractions in logic programming,” in Logic and Computer Science, edited by Pieirgiorgio Odifreddi, Academic Press (APIC Series 31) 1990, 329 – 359.
  8. “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.
  9. “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

  1. “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.
  2. “A Proposal for Modules for λProlog: Preliminary Draft,” Proc. of the 1992 λProlog Workshop, August 1992.
  3. “Abstract Syntax and Logic Programming,” Proc. of the First and Second Russian Conferences on Logic Programming, September 1991, St. Petersburg, LNAI Series, Springer-Verlag.
  4. “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.
  5. “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.
  6. “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

  1. Three entries—titled “Expansion Proofs”, “Focused LK”, and “Focused LJ”—in Towards an Encyclopaedia of Proof Systems, edited by Bruno Woltzenlogel Paleo, January 2017.
  2. “Linear Logic” with Roberto DiCosmo. The Stanford Encyclopedia of Philosophy (Fall 2006 Edition), Edward N. Zalta (ed.).
  3. “Logic, Higher-order,” article for the Second Edition of the Encyclopedia of Artificial Intelligence, ed. S. Shapiro, 1992.


Newsletters and Bulletins

  1. “Formalizing operational semantic specifications in logic.” Concurrency Column of the Bulletin of the European Association for Theoretical Computer Science (EATCS), October 2008.
  2. “Logic and Logic Programming: A Personal Account”, ALP Newsletter, February 2006, 19(1).
  3. “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.
  4. “Proof Theory as an Alternative to Model Theory,” guest editorial for the Newsletter of the ALP, August 1991.


Published Reviews

  1. Review of Advances in Linear Logic, edited by Jean-Yves Girard, Yves Lafont, Laurent Regnier. J. of Symbolic Logic, 62 (2) 1997, pages 678-680.
  2. Review of Invariants, composition, and substitution, by Ekkart Kindler, Acta Inf. 4 (June 1995), 299-312. Computing Reviews, September 1996.
  3. 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.
  4. Review of The art of Prolog: advanced programming techniques, by Leon Sterling and Ehud Shapiro. Computing Reviews, 349 – 350, July 1987.
  5. Review of “Constructive mathematics as a programming logic I: some principles of theory” by Robert Constable. Computing Reviews, April 1987, 213 – 214.


Miscellaneous

  1. “An Extension to ML to Handle Bound Variables in Data Structures,” in the Proc. of the Logical Frameworks BRA Workshop, May 1990.
  2. “Hereditary Harrop formulas and logic programming,” Proc. of the VIII International Congress of Logic, Methodology, and Philosophy of Science, Moscow, August 1987 (abstract).
  3. “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.
  4. “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.
  5. “The sum of an integer’s digits: some properties,” Journal of Undergraduate Mathematics, September 1976, Vol. 8, 61 – 64.

Departmental and University Service at Penn State

Departmental and University Service at UPenn

Courses Taught at MPRI: Master Parisien de Recherche en Informatique

Courses Taught at Ecole polytechnique

Courses Taught at Penn State

Courses Taught at UPenn


This document was translated from LATEX by HEVEA.