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
The videos for the talks given at
LICS 2020 and
ICALP 2020 are now online.
There are many events planned
for World Logic
Day 2021, 14 January 2021. Colleagues in Vienna have assembled
a list of
short statements for their
celebration of this event.
Happy birthday, Andre Scedrov. The volume Logic, Language, and
Security celebrates ScedrovFest65. It includes my short
article Andre and the early days of Penn's Logic and
(draft dated 20 May 2020).
Check out the recently
opened Proof Theory Blog.
I am teaching the first five lectures of the
MPRI course on Linear logic
during 15 September - 13 October 2020. The exam takes plan
virtually on 8 December 2020.
The Abella proof assistant
is based on relational specifications that make use of the notions
of λ-tree syntax and
specifications. Abella is particularly exciting when
applied to meta-theoretic specifications: see, for example, the
specifications of the
λ-calculus and the π-calculus.
I am the General Chair for
LICS: ACM/IEEE Symposium on Logic
in Computer Science until July 2021.
We are currently planning to hold LICS 2021 in Rome
during the week of 27 June.
CIMPA School in Mathematical Logic and Applications, Natal,
Brazil. Rescheduled for December 2021.
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,
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.