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
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 |
books & book chapters |
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
- My paper A system of inference based on proof search: an extended abstract will appear in the proceedings of LICS 2023.
- I gave a talk at the Type Theory, Constructive Mathematics and Geometric Logic meeting on 4 May 2023 at CIRM, Luminy, Marseilles, France.
- I gave a talk at the Ecumenical Logic Meeting on 2-3 March 2023 at UCL, London.
- I gave talks at CSL2023, FICS2023, and LMW2023 in Warsaw during the week of 13 Feb 2023.
- During September and October 2022, I gave 5 lectures in the MPRI course 2-1 Logique linéaire et paradigmes logiques du calcul. Class notes and schedule are available here. The exam for the lectures of Miller and Kesner was held on 12 December 2022.
- Check out the Proof Theory Blog.
- TheoretiCS is a new Diamond Open Access electronic journal covering all areas of Theoretical Computer Science. Please consider submitting your papers to TheoretiCS.
- 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.
- 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.
- The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012 (doi, available via CUP and Amazon). This book covers the design and applications of the λProlog programming language.