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
editorial & professional duties |
teaching & advising |
personal
research projects |
talks |
bio |
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
During Dec 2013 and Jan 2014, I teach 12 hours in the MPRI course 2-1 Logique linéaire et paradigmes logiques du calcul.
I have two internships available for the 2013/2014 M2 season.
CPP 2013, Certified Programs and Proofs, Melbourne, Australia, December 2013 (colocated with APLAS 2013). Steering committee and author of accepted paper.
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, Vienna, Austria. A PC chair. See the call for papers. Submit via EasyChair .
LATD 2014: Logic, Algebra, and Truth Degrees, part of the Vienna Summer of Logic meeting, 16-19 July 2014.
WoLLIC 2014: Workshop on Logic, Language, Information and Computation, Valparaiso Chile, 1-4 September 2014. PC member.
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.