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 sequent calculus
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
Bât. Alan Turing
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
I have two internships available for the 2013/2014 M2 season.
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. See the call for papers.
LATD 2014: Logic, Algebra, and Truth Degrees (part of the Vienna Summer of Logic), 16-19 July 2014. Invited speaker.
∀X.Xπ 2014: All about Proofs, Proofs for All (part of the Vienna Summer of Logic), 18 July 2014. Invited speaker.
WoLLIC 2014: Workshop on Logic, Language, Information and Computation, Valparaiso Chile, 1-4 September 2014. PC member.
During Dec 2013 and Jan 2014, I teach 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.