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 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
Formalized meta-theory:
two-level logic specifications,
structured operational semantics
Automated reasoning: foundational proof certificates
(ProofCert),
unification, interactive theorem proving,
Abella,
Bedwyr
Logic programming:
λProlog,
λ-tree syntax,
linear
logic programming, proof theory foundations
publications |
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
-
W3Proof is
an Inria-funded project that aims to build a framework for trust on
the web.
Our initial goal is to provide tools for users of
the Abella theorem prover
to share and trust theorem files without rechecking proposed proofs.
See the announcement
(in French
and English),
the conference
paper, and the currently available
tools for more information.
-
I have been named
an ACM
Fellow for contributions to proof theory and computational logic.
-
TheoretiCS is a
new Diamond Open Access electronic journal covering all areas of
Theoretical Computer Science. Please consider submitting your papers
to TheoretiCS. I am a member of the Advisory Board.
-
During September and October 2021, I taught
5 lectures in the MPRI
course 2-1
Logique linéaire et paradigmes logiques du calcul.
-
I was the General Chair for
LICS: ACM/IEEE Symposium on Logic
in Computer Science from July 2018 to July 2021.
LICS 2021 was
held online. LICS 2022 will be part
of FLoC 2022, to be held in
Haifa, Israel. The videos for the talks given at
LICS 2020 and
ICALP 2020 are now online.
-
SIGLOG: ACM Special Interest Group
on Logic and Computation.
Apply for membership,
with or without an ACM membership.
-
Check out the recently
opened Proof Theory Blog.
-
The Abella proof assistant
is based on relational specifications that make use of the notions
of λ-tree syntax and
two-level logic
specifications. Abella is particularly exciting when
applied to meta-theoretic specifications: see, for example, the
specifications of the
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.
|