Dale Miller
Director of Research at INRIA Saclay - Île-de-France and the Laboratoire d'Informatique (LIX)
My research covers 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, Abella, Bedwyr, structured operational semantics
Automated reasoning: foundational proof certificates, ProofCert, unification, interactive theorem proving
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)
Address:
INRIA Saclay & LIX
1 rue Honoré d'Estienne d'Orves
Campus de l'École Polytechnique
91120 Palaiseau, France
(map)
Contact:
office: 2053 Bât. Alan Turing
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr
- Two new PhD students and four new post docs will join the ProofCert project and the Parsifal team this coming Fall.
- Joint Meeting of the 23rd EACSL Annual Conference on Computer Science Logic (CSL) and the 29th ACM / IEEE Symposium on Logic in Computer Science (LICS). 14-18 July 2014 (part of the Vienna Summer of Logic). A PC chair.
- LATD 2014: Logic, Algebra, and Truth Degrees (Vienna, 16-19 July). Invited speaker.
- ∀X.Xπ 2014: All about Proofs, Proofs for All (Vienna, 18 July). Invited speaker.
- WoLLIC 2014: Workshop on Logic, Language, Information and Computation, Valparaiso Chile, 1-4 September 2014. PC member.
- I taught a graduate course in Pisa (10-16 April 2014).
- During Dec 2013 and Jan 2014, I taught 12 hours in the MPRI course 2-1 Logique linéaire et paradigmes logiques du calcul.
- The book Programming with Higher-Order Logic by Gopalan Nadathur and me was published by Cambridge University Press in June 2012. This book covers the design and applications of the λProlog programming language.