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)

Postal Address:
INRIA Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
B√Ętiment Alan Turing
CS35003
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

Appearing soon
News and events