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