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 | 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

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

• Workshop on Proof Theory and its Applications, 6-7 September 2018 in Ghent (associated with the Proof Society Summer School 2018). Invited speaker. Abstract.
• MLTS is a new functional programming language that provides new features for the manipulation of bindings in syntactic expressions. A draft description is available as a browser-based (no installation required) implementation of the language. This language was presented at LFMTP 2018 and will be presented at HOPE 2018.
• Third Tübingen Conference on Proof-Theoretic Semantics, 27-30 March 2019. Invited speaker.
• MPRI Course 2-1: Linear Logic. Master-level (M2) course taught at the University of Paris Diderot. Instructor.
• EPIC is a STIC-AmSud project funded by CAPES (Brazil), COLCIENCIAS (Colombia) and INRIA (France). Member.
• Three glossy articles about ProofCert are available: Improving trust in computer systems using formal proofs (in Adjacent Open Access) (pdf), The hunt for a broad-spectrum proof certificate (in Science Impact) and Developing the infrastructure for formal proofs (in EU Researcher)
• Dale Fest. It was a wonderful event! Thanks to the organizer and those who contributed their best wishes, anecdotes, and their lastest research work.
• The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012 (available via CUP and Amazon). This book covers the design and applications of the λProlog programming language.