Dale Miller
Director of Research (DRCE) at
Inria
Saclay - Île-de-France and the
Laboratoire d'Informatique
(LIX), UMR 7161
Member of Partout, a team
joint between Inria and LIX
Directions
for visitors
Time and
weather in Orsay & Palaiseau
|
|
My research in Computational Logic includes the
following topics.
Proof theory:
Classical, intuitionistic,
and linear
logics; focused proof systems; fixed points;
higher-order quantification
Automated reasoning: foundational proof certificates
(ProofCert),
unification, interactive theorem proving,
Abella,
Bedwyr
Logic programming:
proof theory foundations,
λProlog,
λ-tree syntax,
linear logic programming
Formalized meta-theory:
two-level logic specifications,
structured operational semantics
journal & conference papers |
books & book chapters |
tech reports & short articles
talks |
editorial & professional duties |
teaching & advising
cv (pdf) |
research themes |
bio |
personal |
photos
|
Postal Address:
Inria Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
91120 Palaiseau, France
Contact:
office: 2053 Bât. Alan Turing
(map)
phone: +33 (0)1 77 57 80 53
email: dale.miller at inria.fr
|
|
News and events
-
I am on the PC of the following meetings in 2024 and 2025:
CICM24,
HCVS2024,
NCL'24,
LPAR 2024, and
CSL2025.
-
I am a PC co-Chair
for FLOPS
2024 to be held in Kumamoto, Japan, 15-17 May 2024.
-
I gave three hours of lectures during the
Days
in Logic, 1-3 February 2024, at the Technical University of Lisbon.
My slides.
-
I am honored to have been selected as one of the recipients of the
Dov Gabbay Prize for Logic
and Foundations for 2023. The award ceremony was
held
online 25 October 2023.
-
During September and October 2023, I gave
4 lectures in the MPRI
course 2-1
Logique linéaire et paradigmes logiques du calcul.
Class notes and schedules are available
here.
-
Check out the Proof Theory Blog.
-
The Abella proof assistant
is based on relational specifications that use the notions
of λ-tree syntax and
two-level logic
specifications. Abella is particularly useful 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
Science)
on structural
proof theory, automated reasoning and computation in celebration of
Dale Miller’s 60th birthday, Volume 29, Special Issue 8,
September 2019.
-
The
book Programming
with Higher-Order Logic
by Gopalan
Nadathur and me was published by Cambridge University Press in
June 2012 (doi, available
via CUP and
Amazon).
This book covers the design and applications of
the λProlog programming language.
|