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
FSCD 2017: Formal
Structures for Computation and Deduction. Program committee
chair. The current draft of
LL2016 - Linear Logic:
interaction, proofs and computation, 7-10 November 2016, Lyon. France.
Invited speaker at the Workshop on linear logic, mathematics and
AiML 2016: Advances in
Modal Logic. Accepted paper.
FSCD 2016: Formal
Structures for Computation and Deduction. Accepted paper.
Porto, 25 June 2016. Invited speaker.
between logic, computer science and linguistics: history and
philosophy, Lille, 15 June 2016.
Workshop on Proofs, justifications and certificates. 3-4 June 2016,
Toulouse, France. Invited Lecturer.
TYPES 2016: 22nd
International Conference on Types for Proofs and Programs.
Novi Sad, Serbia, 23-26 May 2016. Invited speaker.
Tutorial speaker at the
centre, Ca’ Foscari University, Venice, 27 April 2016.
Course 2-1: Linear Logic. PhD course at the University of
Paris Diderot. Instructor.
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.