Dale Miller
Director of Research at
INRIA
Saclay - Île-de-France and the
Laboratoire d'Informatique
(LIX)
My research touches 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
- Communicating and trusting proofs: The case for foundational proof certificates by Dale Miller. To appear 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.
- The Parsifal team is offering some internships for 2015.
- 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.
- LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications (Natal, Brazil, 31 August - 1 September 2015). Invited speaker.
- 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.