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

F. GilbertExtending higher-order logic with predicate subtyping.  Thèse de doctorat, Université Paris 7, Paris, France, April 2018. PDF | BibTeX )
G. BurelLinking Focusing and Resolution with Selection.  Research Report hal-01670476, HAL Research Report, April 2018. Web page | PDF | BibTeX )
C. L. SubramaniamCubical Type Theory in Dedukti.  Rapport de Master, Master Parisien de Recherche en Informatique, Paris, France, September 2017. BibTeX )
F. ThiréExporting an Arithmetic Library from Dedukti to HOL.  Research Report hal-01668250, HAL Research Report, December 2017. Web page | PDF | BibTeX )
F. BlanquiSize-based termination of higher-order rewritingJournal of Functional Programming 28, April 2018. Web page | PDF | BibTeX )

All the Deducteam publications