Dale Miller
Director of Research at
Inria
Saclay - Île-de-France and the
Laboratoire d'Informatique
(LIX)
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
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
- IJCAR-2018: 9th International Joint Conference on Automated Reasoning, Oxford, 14-17 July 2018. Program committee member.
- LAP 2017: 6th Conference on Logic and Applications, Dubrovnik, Croatia. Invited participant.
- FSCD 2017: Formal Structures for Computation and Deduction, 3-9 September 2017, Oxford. Program committee chair. The proceedings for the meeting are now online.
- 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)
- MPRI Course 2-1: Linear Logic. PhD course at the University of Paris Diderot. Instructor.
- 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 Amazon). This book covers the design and applications of the λProlog programming language.