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
Jean-Pierre JOUANNAUD
Emeritus professor, ENS Paris-Saclay

Associated and Temporary Staff

Pablo ARRIGHI
Temporary assignment, Aix-Marseille University
Michael FÄRBER
Post-doctoral researcher, Inria
Rehan Malak
Post-doctoral researcher, DigiCosme
Étienne MIQUEY
Post-doctoral researcher, CNRS

Ph.D. Students

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

Administrative and Technical Staff

Emmanuelle PERROT
Gestionnaire Inria

Website

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

About LSV

    

About Deducteam

A joint team with

Logo INRIA Saclay