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.
During Jan and Feb 2015, I teach 12 hours in
course 2-1 Logique
linéaire et paradigmes logiques du calcul.
- Just published:
Foundational Proof Certificates by Dale Miller.
In the proceedings
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.
2015: 10th Workshop on Logical and Semantic Frameworks, with
Applications (Natal, Brazil, 31 August - 1 September 2015).
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
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