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
If you are interested in being on the ballot for the Executive
Committee of the SIGLOG executive committee, please contact me
before 25 November 2015. The vote will take place in 2016. The
open positions are Chair, Vice-Chair, Treasurer, and Secretary.
on Efficient and Natural Proof Systems,
University of Bath, December 14th-16th, 2015.
2015: 10th Workshop on Logical and Semantic Frameworks, with
Applications (Natal, Brazil, 31 August - 1 September 2015). Part
of NAT@Logic 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.
- 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.
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.
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