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
effort is offering one or two
positions starting in Fall 2015.
- After serving six years as the
Editor-in-Chief of the Transactions
on Computational Logic, I am delighted to announce that
Orna Kupferman has
been selected as the new Editor-in-Chief starting in July 2015.
on History and Philosophy of Computing (7 August) 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). Part
of NAT@Logic 2015.
25th International Symposium on Logic-Based Program Synthesis and
Transformation (Siena, 13-15 July 2015). Invited speaker.
ETH Zurick Department of Computer Science
Colloquium Series, 20 April 2015. Invited speaker.
- Recently published:
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