Dale Miller

Director of Research at
Inria Saclay - Île-de-France and the Laboratoire d'Informatique (LIX)

Team leader of Parsifal
ERC Advanced Grant ProofCert

I work on the following topics in Computational Logic.

Proof theory: Classical, intuitionistic, and linear logics; focused proof systems; fixed points; higher-order quantification

Formalized meta-theory: two-level logic specifications, structured operational semantics

Automated reasoning: foundational proof certificates, unification, interactive theorem proving, Abella, Bedwyr

Logic programming: λProlog, λ-tree syntax, linear logic programming

papers | books & book chapters | tech reports & short articles
talks | editorial & professional duties | teaching & advising
research themes | bio | personal | cv (pdf)

Postal Address:
Inria Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
CS35003
91120 Palaiseau, France

Contact:
office: 2053 Bât. Alan Turing (map)
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr

Directions for visitors
Time and weather in Paris

• The Parsifal team is offering some internships for 2015.
• Session on History and Philosophy of Computing at the 15th Congress of Logic, Methodology and Philosophy of Science, Helsinki, 3-8 August 2015. Invited speaker.
• LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications (Natal, Brazil, 31 August - 1 September 2015). Invited speaker.
• LOPSTR 2015: 25th International Symposium on Logic-Based Program Synthesis and Transformation (Siena, 13-15 July 2015). Invited speaker.
• Appearing soon: Communicating and trusting proofs: The case for foundational proof certificates by Dale Miller in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011. Edited by Pierre Edouard Bour.
• During Jan and Feb 2015, I teach 12 hours in the MPRI course 2-1 Logique linéaire et paradigmes logiques du calcul.
• Just published: Foundational Proof Certificates by Dale Miller. In the proceedings of All about Proofs, Proofs for All (APPA), edited by D. Delahaye and B. Woltzenlogel Paleo, pp. 150-163.
• Just published: A tutorial titled Abella: A System for Reasoning about Relational Specifications by David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, and Yuting Wang. Journal of Formalized Reasoning, 7(2), 2014, pp. 1-89.
• Recently published: Automation of Higher-Order Logic by Christoph Benzmüller and Dale Miller. Handbook of the History of Logic, Volume 9: Logic and Computation, edited by D. Gabbay, J. Siekmann, and J. Woods (North-Holland), pp. 215-254.
• Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th ACM / IEEE Symposium on Logic in Computer Science (LICS). 14-18 July 2014 (part of the Vienna Summer of Logic). A PC chair.
• The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012. This book covers the design and applications of the λProlog programming language.