Dale Miller
Director of Research at
INRIA
Saclay  ÎledeFrance and the
Laboratoire d'Informatique
(LIX)
Team leader of Parsifal
ERC Advanced Grant ProofCert


My research touches on the following topics in Computational
Logic.
Proof theory:
Classical, intuitionistic, and linear logics; focused
proof systems; fixed points; higherorder quantification
Formalized metatheory:
twolevel logic specifications,
structured operational semantics
Automated reasoning: foundational proof certificates,
unification, interactive theorem proving,
Abella,
Bedwyr
Logic programming:
λProlog,
λtree syntax,
linear
logic programming
papers 
books & book chapters 
tech reports & short articles
talks 
editorial & professional duties 
teaching & advising
research themes 
bio 
personal 
cv (pdf)

Postal Address:
INRIA Saclay & LIX
Campus de l'École Polytechnique
1 rue Honoré d'Estienne d'Orves
Bâtiment Alan Turing
CS35003
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
Directions
for visitors
Time and weather in Paris


Appearing soon
 A tutorial titled
Abella: A System for Reasoning about Relational Specifications by
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan
Nadathur, Alwen Tiu, and Yuting Wang. To appear in
the Journal of Formalized Reasoning.
Draft dated 20 Nov 2014.

Revision to: Linear Logic
by Roberto
Di Cosmo and Dale Miller. The Stanford Encyclopedia of
Philosophy, Edward N. Zalta (ed.).

Automation of HigherOrder
Logic by Christoph Benzmüller and Dale Miller.
To appear in the Handbook of the History of Logic, Volume
9: Logic and Computation, edited by D. Gabbay, J. Siekmann,
and J. Woods (NorthHolland).

Communicating and trusting proofs:
The case for foundational proof certificates
by Dale Miller. To appear in the
Proceedings of the
14th Congress of Logic,
Methodology and Philosophy of Science in Nancy, France, 1926
July 2011. Edited by Pierre Edouard Bour.
News and events
