Director of Research at
Saclay - Île-de-France and the
(LIX), UMR 7161
Member of Partout, a team
joint between Inria and LIX
Arriving from Paris by public transportation
Updated directions during
construction phase (starting Oct 2019)
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
Chuck Liang and I have recently completed and submitted a paper
titled Focusing Gentzen's LK proof system. This paper proves
the main metatheory results for the LKF proof system: the only
prerequisite is basic knowledge of the sequent calculus. See
the draft dated 3 April
I have funding for a Ph.D. student, starting in Fall 2020. See the
UPDATE 1 April 2020: Given the coronavirus pandemic and
associated travel restrictions,
LICS 2020 will be
held online and joint
with ICALP 2020.
Our colleagues at Saarbrücken, Germany will be organizing this
online meeting around the dates originally planned (8-11 July 2020).
Many details still need to be settled.
The 2021 meeting will be held in Rome during the week of 26 June. I am the General Chair for
LICS: ACM/IEEE Symposium on Logic
in Computer Science until July 2021.
MPRI Course 2-1: Linear Logic. Master-level
(M2) course taught at the University of Paris Diderot. Instructor.
I am grateful to the editors and authors for their contributions to
a special issue of MSCS (Mathematical Strcutures in Computer
proof theory, automated reasoning and computation in celebration of
Dale Miller’s 60th birthday, Volume 29, Special Issue 8,
IJCAR-2020: 10th International
Joint Conference on Automated Reasoning, Paris, 29 June - 2
July 2020. PC member.
CIMPA School in Mathematical Logic and Applications, Natal,
Brazil, 9-18 December 2020.
International Conference on Logic for Programming, Artificial
Intelligence and Reasoning Alicante, Spain on 22-27 May, 2020.
TEASE-LP: Workshop on
Trends, Extensions, Applications and Semantics of Logic
Programming, Dublin, 25 April 2020 (associated with ETAPS
2020). PC member.
The Parsifal team has
been retired. Parsifal was an Inria Saclay team from 2007-2019 and
a LIX team from 2004-2019.
SIGLOG: ACM Special Interest Group
on Logic and Computation.
Apply for membership,
with or without an ACM membership.
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.