Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
ERC Advanced Grant ProofCert
I do research on the following topics in Computational Logic.
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,
books & book chapters |
tech reports & short articles
editorial & professional duties |
teaching & advising
research themes |
Inria Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
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
Porto, 25 June 2016. Invited speaker.
TYPES 2016: 22nd
International Conference on Types for Proofs and Programs.
Novi Sad, Serbia, 23-26 May 2016. Invited speaker.
between logic, computer science and linguistics: history and
philosophy, Lille, 15 June 2016.
2015: 10th Workshop on Logical and Semantic Frameworks, with
Applications (Natal, Brazil, 31 August - 1 September 2015). Part
of NAT@Logic 2015.
on History and Philosophy of Computing (7 August) at
the 15th Congress of Logic,
Methodology and Philosophy of Science, Helsinki, 3-8 August
2015. Invited speaker.
- After serving six years as the
Editor-in-Chief of the Transactions
on Computational Logic, I am delighted to announce that
Orna Kupferman has
been selected as the new Editor-in-Chief starting in July 2015.
25th International Symposium on Logic-Based Program Synthesis and
Transformation (Siena, 13-15 July 2015). Invited speaker.
ETH Zurick Department of Computer Science
Colloquium Series, 20 April 2015. Invited speaker.
with Higher-Order Logic
Nadathur and me was published by Cambridge University Press in
June 2012 (available
This book covers the design and applications of
the λProlog programming language.