Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
Principal investigator of ProofCert
My research covers the following topics in Computational
Classical, intuitionistic, and linear logics, focused sequent calculus
proof systems, fixed points, higher-order quantification
two-level logic specifications,
structured operational semantics
Automated reasoning: foundational proof certificates,
unification, interactive theorem proving
λ-tree syntax, linear logic programming
books & book chapters |
tech reports & short articles
editorial & professional duties |
teaching & advising |
research projects |
INRIA Saclay & LIX
Bât. Alan Turing
1 rue Honoré d'Estienne d'Orves
Campus de l'École Polytechnique
91120 Palaiseau, France
office: 2053 Bât. Alan Turing
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr
Time and weather in Paris
News and events
During Dec 2013 and Jan 2014, I teach 12 hours in
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.
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.
for papers. Submit
via EasyChair .
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
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