Director of Research at
Saclay - Île-de-France and the
Team leader of Parsifal
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
2017: Formal Structures for Computation and Deduction, 3-9
September 2017, Oxford. Program committee chair.
is online (also
TLLA 17: Trends in
Linear Logic and Applications. Accepted abstract titled ``Using
linear logic and proof theory to unify computational logic''.
Draft dated 21 July 2017.
IJCAR-2018: 9th International
Joint Conference on Automated Reasoning, Oxford, 14-17 July 2018.
Program committee member.
Three glossy articles
trust in computer systems using formal proofs
(in Adjacent Open
for a broad-spectrum proof certificate
(in Science Impact)
the infrastructure for formal proofs
(in EU Researcher)
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.
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.