Dale Miller

Director of Research at
Inria Saclay - Île-de-France and the Laboratoire d'Informatique (LIX), UMR 7161

Team leader of Parsifal
ERC Advanced Grant ProofCert

My research in Computational Logic includes the following topics.

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

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

Automated reasoning: foundational proof certificates, unification, interactive theorem proving, Abella, Bedwyr

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
91120 Palaiseau, France

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

Directions for visitors
Time and weather in Paris

News and events