Dale Miller

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

Member of Partout, a team joint between Inria and LIX

Directions for visitors
Time and weather in Orsay & Palaiseau

My research in Computational Logic includes the following topics.

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

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

Logic programming: proof theory foundations, λProlog, λ-tree syntax, linear logic programming

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

publications | edited proceedings | tech reports & short articles
talks | editorial & professional duties | teaching & advising
cv (pdf) | research themes | bio | personal | photos

Postal Address:
Inria Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91120 Palaiseau, France

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

• In Memoriam: Peter B. Andrews (November 1, 1937 – April 21, 2025)
• My book Proof Theory and Logic Programming: Computation as Proof Search should be published by Cambridge University Press in Winter 2025. A pre-publication draft is available.
• I presented a talk titled Proof Theory and Type Theory: Distinct Foundations for Designing Proof Assistants at the Proof Representations: From Theory to Applications meeting in Banff, Canada on 3 June 2025. My lighning talk was based on these slides
• Check out the Proof Theory Blog.
• The Abella proof assistant is based on relational specifications that use the notions of λ-tree syntax and two-level logic specifications. Abella is most useful when applied to meta-theoretic specifications: see, for example, the specifications of the λ-calculus and the π-calculus.
• I am grateful to the editors and authors for their contributions to a special issue of MSCS (Mathematical Structures in Computer Science) on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday, Volume 29, Special Issue 8, September 2019.
• Cambridge University Press published in 2012 the book Programming with Higher-Order Logic by Gopalan Nadathur and me (doi, available via CUP and Amazon). This book covers the design and applications of the λProlog programming language.