Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
ERC Advanced Grant ProofCert
My research covers the following topics in Computational
Classical, intuitionistic, and linear logics; focused
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 themes |
INRIA Saclay & LIX
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
Two new PhD students and four new post docs
will join the
ProofCert project and
the Parsifal team this
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.
Logic, Algebra, and Truth Degrees (Vienna, 16-19 July). Invited speaker.
2014: All about Proofs, Proofs for All (Vienna, 18 July).
- 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
course 2-1 Logique
linéaire et paradigmes logiques du calcul.
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