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