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

I do research on 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, 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.miller at inria.fr

Directions for visitors
Time and weather in Paris

News and events
  • FSCD 2017: Formal Structures for Computation and Deduction. Program committee chair. The current draft of the call-for-papers.
  • LL2016 - Linear Logic: interaction, proofs and computation, 7-10 November 2016, Lyon. France. Invited speaker at the Workshop on linear logic, mathematics and computer science. Slides.
  • MPRI Course 2-1: Linear Logic. PhD course at the University of Paris Diderot. Instructor.
  • Dagstuhl semainar on Universality of Proofs. My slides for a 10 minute talk.
  • AiML 2016: Advances in Modal Logic. Accepted paper.
  • FSCD 2016: Formal Structures for Computation and Deduction. Accepted paper.
  • Linearity 2016 Porto, 25 June 2016. Invited speaker.
  • TYPES 2016: 22nd International Conference on Types for Proofs and Programs. Novi Sad, Serbia, 23-26 May 2016. Invited speaker. Abstract and slides.
  • The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012 (available via Amazon). This book covers the design and applications of the λProlog programming language.