Dale Miller - Home page

Dale Miller

Director of Research 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
Arriving from Paris by public transportation
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

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.miller at inria.fr

News and events

I will speak to the Online Worldwide Seminar on Logic and Semantics (OWLS) on 10 March 2021 about "A proof theory for model checking".
I spoke about "Focusing Gentzen's LK proof system" to the Proof Theory Virtual Seminar on 3 March 2021. My slides and a related paper (co-authored with Chuck Liang) are available.
I am the General Chair for LICS: ACM/IEEE Symposium on Logic in Computer Science until July 2021. LICS 2021 will be held online. The videos for the talks given at LICS 2020 and ICALP 2020 are now online.
There are many events planned for World Logic Day 2021, 14 January 2021. Colleagues in Vienna have assembled a list of short statements for their celebration of this event.
Check out the recently opened Proof Theory Blog.
The Abella proof assistant is based on relational specifications that make use of the notions of λ-tree syntax and two-level logic specifications. Abella is particularly exciting when applied to meta-theoretic specifications: see, for example, the specifications of the the λ-calculus and the π-calculus.
Logic@Natal: CIMPA School in Mathematical Logic and Applications, Natal, Brazil. Rescheduled for December 2021.
I am grateful to the editors and authors for their contributions to a special issue of MSCS (Mathematical Strcutures 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.
SIGLOG: ACM Special Interest Group on Logic and Computation. Apply for membership, with or without an ACM membership.
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.