Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
ERC Advanced Grant ProofCert
I do research on the following topics in Computational Logic.
logics; focused proof systems; fixed points; higher-order quantification
two-level logic specifications,
structured operational semantics
Automated reasoning: foundational proof certificates,
unification, interactive theorem proving,
books & book chapters |
tech reports & short articles
editorial & professional duties |
teaching & advising
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 at lix.polytechnique.fr
Time and weather in Paris
News and events
article on Developing the infrastructure for formal
proofs that appears in EU
2017: Formal Structures for Computation and Deduction. Program
is online (also
talk at LIX, 23 Feb 2017. I spoke on "Communicating and trusting formal proofs".
Course 2-1: Linear Logic. PhD course at the University of
Paris Diderot. Instructor.
2017: 6th Conference on Logic and Applications, Dubrovnik, Croatia. Invited participant.
2017. Invited speaker. Slides
Fest. It was a wonderful event! Thanks to the organizer and
those who contributed their best wishes, anecdotes, and their
lastest research work.
TYPES 2016: 22nd
International Conference on Types for Proofs and Programs.
Novi Sad, Serbia, 23-26 May 2016. Invited speaker.
with Higher-Order Logic
Nadathur and me was published by Cambridge University Press in
June 2012 (available
This book covers the design and applications of
the λProlog programming language.