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
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
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
publications |
edited volumes |
tech reports & short articles
talks |
editorial & professional duties |
teaching & advising
cv (pdf) |
research themes |
bio |
personal |
photos