Director of Research at
Saclay - Île-de-France and the
(LIX), UMR 7161
Team leader of Parsifal
Time and weather in Paris
My research in Computational Logic includes the
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
News and events
MPRI Course 2-1: Linear Logic. Master-level
(M2) course taught at the University of Paris Diderot. Instructor.
- Faculty positions for 2019 in the CS Department of
École Polytechnique are announced
LICS: The ACM/IEEE Symposium
on Logic in Computer Science. The
2019 meeting will be
held in Vancouver, BC, 24-24 July 2019.
LFMTP 2019: Logical
Frameworks and Meta-Languages: Theory and Practice. Affiliated with
LICS 2019, Vancouver, Canada. June 22, 2019. Co-PC chair.
MLTS is a new functional programming language that provides new
features for the manipulation of bindings in syntactic expressions.
A draft description is
available, as is a browser-based (no installation
of the language. This language was presented
at LFMTP 2018 and
Tübingen Conference on Proof-Theoretic Semantics, 27-30
March 2019. Invited speaker.
Proof Theory and its Applications, 6-7 September 2018 in Ghent
Society Summer School 2018). Invited speaker.
a STIC-AmSud project funded by CAPES (Brazil), COLCIENCIAS (Colombia)
and INRIA (France). Member.
Three glossy articles
trust in computer systems using formal proofs
(in Adjacent Open
for a broad-spectrum proof certificate
(in Science Impact) and
the infrastructure for formal proofs
(in EU Researcher)
Fest. It was a wonderful event! Thanks to the organizer and
those who contributed their best wishes, anecdotes, and their
lastest research work.
with Higher-Order Logic
Nadathur and me was published by Cambridge University Press in
June 2012 (available
via CUP and
This book covers the design and applications of
the λProlog programming language.