DEDUCTEAM:

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, ...

Members

Permanent Staff

Bruno BARRAS
Researcher, Inria Saclay-Île de France
Frédéric BLANQUI
Researcher, Inria Saclay-Île de France
Valentin BLOT
Researcher, Inria Saclay-Île de France
Gilles DOWEK
Senior researcher, Inria Saclay-Île de France

Associated and Temporary Staff

Guillaume BUREL
Inria researcher (assistant professor, ESIEE)
Franck SLAMA
Post-doctoral researcher, Inria

Ph.D. Students

Yacine EL HADDAD
PhD student, DigiCosme
Gaspard FÉREY
PhD student
Guillaume GENESTIER
PhD student
François THIRÉ
PhD student, ENS Paris-Saclay

Administrative and Technical Staff

Adeline LOCHET
Gestionnaire Inria
Emmanuelle PERROT
Gestionnaire Inria

Website

http://deducteam.gforge.inria.fr/

About LSV

About Deducteam

A joint team with

Logo INRIA Saclay