Section: Overall Objectives

Objectives

The project-team investigates applications of proof theory to the design of logical frameworks, to 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, systems translating proofs between external proof systems and Dedukti theories, tools to migrate proofs within Dedukti from one theory to another, tools to prove the confluence, the termination, and the consistency of theories expressed in Dedukti , and tools to develop proofs directly in Dedukti .