Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
ERC Advanced Grant ProofCert
My research touches on the following topics in Computational
Classical, intuitionistic, and linear logics; focused
proof systems; fixed points; higher-order quantification
two-level logic specifications,
structured operational semantics
Automated reasoning: foundational proof certificates,
unification, interactive theorem proving,
books & book chapters |
tech reports & short articles
editorial & professional duties |
teaching & advising
research themes |
INRIA Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91120 Palaiseau, France
office: 2053 Bât. Alan Turing
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr
Time and weather in Paris
- 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. To appear in
the Journal of Formalized Reasoning.
Draft dated 20 Nov 2014.
Revision to: Linear Logic
Di Cosmo and Dale Miller. The Stanford Encyclopedia of
Philosophy, Edward N. Zalta (ed.).
Automation of Higher-Order
Logic by Christoph Benzmüller and Dale Miller.
To appear in the Handbook of the History of Logic, Volume
9: Logic and Computation, edited by D. Gabbay, J. Siekmann,
and J. Woods (North-Holland).
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.
News and events