Sites Inria

English version

Equipe de recherche DEDUCTEAM

Rapports d'activité

Objectives

The project-team investigates the design of logical frameworks, in order to ensure interoperability between proof systems, and to the development of system-independent proof libraries. To achieve these goals, we develop

a logical framework Dedukti, where several theories can be expressed,

tools to import proofs developed in external proof systems to Dedukti theories,

tools to translate proofs from one Dedukti theory to another,

tools to export proofs expressed in Dedukti theories to an external proof system,

tools to prove the confluence, the termination, and the consistency of theories expressed in Dedukti,

tools to develop proofs directly in Dedukti,

an encyclopedia Logipedia of proofs expressed in various Dedukti theories.

Suivez Inria