The Deducteam axis focuses developping logical frameworks, that is proof-checkers able to verify proofs developed in other, interactive or automatic, systems. Its main activity is to develop Dedukti, a logical framework based in the lambda-Pi-calculus modulo theory and to express in it proofs developed both in constructive and classical proof systems : HOL, Matita, FoCaLiZe, Zenon, iProver, veriT, ...


Permanent Members

Bruno Barras
Researcher, Inria Saclay-Île de France
Frédéric Blanqui
Researcher, Inria Saclay-Île de France
Gilles Dowek
Senior researcher, Inria Saclay-Île de France

Associated and Temporary Members

Valentin Blot
Rodolphe Lepigre
Post-doctoral researcher, Inria
Guillaume Burel
Inria researcher (assistant professor, ESIEE)
Franck Slama
Post-doctoral researcher, Inria

Ph.D. Students

Guillaume Bury
PhD student
Gaspard Férey
PhD student
François Thiré
PhD student, ENS Paris-Saclay
Yacine El Haddad
PhD student, DigiCosme
Guillaume Genestier
PhD student


About LSV

About Deducteam

A joint team with

Logo INRIA Saclay

Recent Publications

All the Deducteam publications

S. Colin, R. Lepigre and G. SchererUnboxing Mutually Recursive Type DefinitionsIn JFLA'19. January 2019. To appear. PDF | BibTeX )
R. Lepigre and C. RaffalliAbstract Representation of Binders in OCaml using the Bindlib LibraryIn LFMTP'18, pages 42-56. ACM Press, July 2018. Web page | PDF | BibTeX )
R. LepigrePML2: Integrated Program Verification in MLIn TYPES'17, Leibniz International Proceedings in Informatics. Leibniz-Zentrum für Informatik, 2018. To appear. PDF | BibTeX )
R. Lepigre and C. RaffalliPractical Subtyping for Curry-Style LanguagesACM Transactions on Programming Languages and Systems, 2018. To appear. PDF | BibTeX )
F. GilbertExtending higher-order logic with predicate subtyping.  Thèse de doctorat, Université Paris 7, Paris, France, April 2018. PDF | BibTeX )

All the Deducteam publications