Director of Research at
Saclay - Île-de-France and the
(LIX), UMR 7161
Team leader of Parsifal
Time and weather in Paris
My research in Computational Logic includes the
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
News and events
LFMTP 2019: Logical
Frameworks and Meta-Languages: Theory and Practice. Affiliated with
LICS 2019, Vancouver, Canada. June 22, 2019. Co-PC chair.
LICS: The ACM/IEEE Symposium
on Logic in Computer Science.
2019 meeting will be
held in Vancouver, BC, 24-27 July 2019.
2020 meeting will be
held in Beijing, 8-12 July 2020. The 2021 meeting will be held in
SIGLOG: ACM Special Interest Group on Logic and Computation.
Proof Theory for
Automated Deduction, Automated Deduction for Proof Theory, 23-25
October 2019, Funchal, Madeira. Invited speaker.
MLTS is a new functional programming language that provides new
features for the manipulation of bindings in syntactic expressions.
A draft description is
available, as is a browser-based (no installation
of the language. This language was presented
at LFMTP 2018 and
Three glossy articles
trust in computer systems using formal proofs
(in Adjacent Open
for a broad-spectrum proof certificate
(in Science Impact) and
the infrastructure for formal proofs
(in EU Researcher)
Fest. It was a wonderful event! Thanks to the organizer and
those who contributed their best wishes, anecdotes, and their
lastest research work.
with Higher-Order Logic
Nadathur and me was published by Cambridge University Press in
June 2012 (available
via CUP and
This book covers the design and applications of
the λProlog programming language.