Dale Miller

Director of Research at INRIA Saclay - Île-de-France and the Laboratoire d'Informatique (LIX)

Team leader of Parsifal
ERC Advanced Grant ProofCert

My research covers the following topics in Computational Logic.

Proof theory: Classical, intuitionistic, and linear logics; focused proof systems; fixed points; higher-order quantification

Formalized meta-theory: two-level logic specifications, Abella, Bedwyr, structured operational semantics

Automated reasoning: foundational proof certificates, ProofCert, unification, interactive theorem proving

Logic programming: λProlog, λ-tree syntax, linear logic programming

papers | books & book chapters | tech reports & short articles
talks | editorial & professional duties | teaching & advising
research themes | bio | personal | cv (pdf)

Address:
INRIA Saclay & LIX
1 rue Honoré d'Estienne d'Orves
Campus de l'École Polytechnique
91120 Palaiseau, France (map)

Contact:
office: 2053 Bât. Alan Turing
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr

Directions for visitors
Time and weather in Paris

• Two new PhD students and four new post docs will join the ProofCert project and the Parsifal team this coming Fall.
• Joint 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.
• LATD 2014: Logic, Algebra, and Truth Degrees (Vienna, 16-19 July). Invited speaker.
• WoLLIC 2014: Workshop on Logic, Language, Information and Computation, Valparaiso Chile, 1-4 September 2014. PC member.
• I taught a graduate course in Pisa (10-16 April 2014).
• During Dec 2013 and Jan 2014, I taught 12 hours in the MPRI course 2-1 Logique linéaire et paradigmes logiques du calcul.
• The book Programming with Higher-Order Logic 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 language.