Dale Miller

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

Team leader of Parsifal

Directions for visitors
Time and weather in Paris

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 (ProofCert), 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 | photos | 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.miller at inria.fr

News and events