Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
ERC Advanced Grant ProofCert
I work on the following topics in Computational Logic.
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
News and events
- The Parsifal team is offering some
internships for 2015.
Speaker in the ETH Zurick Department of Computer Science
Distinguished Colloquium Series, 20 April 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.
2015: 10th Workshop on Logical and Semantic Frameworks, with
Applications (Natal, Brazil, 31 August - 1 September 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.
The book Programming with
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