Director of Research (DRCE) at
Saclay - Île-de-France and the
(LIX), UMR 7161
Member of Partout, a team
joint between Inria and LIX
and weather in Palaiseau
My research in Computational Logic includes the
logics; focused proof systems; fixed points;
Automated reasoning: foundational proof certificates
unification, interactive theorem proving,
proof theory foundations,
linear logic programming
two-level logic specifications,
structured operational semantics
books & book chapters |
tech reports & short articles
editorial & professional duties |
teaching & advising
cv (pdf) |
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
My paper A system of inference based
on proof search: an extended abstract will appear in the
proceedings of LICS 2023.
I gave a talk at
Theory, Constructive Mathematics and Geometric Logic meeting on 4
May 2023 at CIRM, Luminy, Marseilles, France.
I gave a talk at
Logic Meeting on 2-3 March 2023 at UCL, London.
I gave talks at CSL2023,
in Warsaw during the week of 13 Feb 2023.
During September and October 2022, I gave
5 lectures in the MPRI
Logique linéaire et paradigmes logiques du calcul.
Class notes and schedule are available
The exam for the lectures of Miller and Kesner was held on 12 December 2022.
Check out the Proof Theory Blog.
TheoretiCS is a
new Diamond Open Access electronic journal covering all areas of
Theoretical Computer Science. Please consider submitting your papers
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 grateful to the editors and authors for their contributions to
a special issue of MSCS (Mathematical Structures in Computer
proof theory, automated reasoning and computation in celebration of
Dale Miller’s 60th birthday, Volume 29, Special Issue 8,
with Higher-Order Logic
Nadathur and me was published by Cambridge University Press in
June 2012 (doi, available
via CUP and
This book covers the design and applications of
the λProlog programming language.