|
 
|
[BB12] CoqInE : Translating the calculus of inductive constructions into the λΠ-calculus modulo.
Conférences Internationales sans actes : Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012), Manchester, United Kingdom,Mots clés: proof translation, universal proof language, inductive types, dependant types, rewriting
Résumé:
We show how to translate the Calculus of Inductive Constructions (CIC) as implemented by Coq into the λΠ-calculus modulo, a proposed common backend proof format for heterogeneous proof assistants.
Equipe:
sys
Collaboration:
Computation and Logic Group, McGill University
BibTeX
| @conference { | |||
| BB12, | |||
| title | = | "{CoqInE : Translating the calculus of inductive constructions into the λΠ-calculus modulo.}", | |
| author | = | " M. Boespflug and G. Burel ", | |
| year | = | 2012, | |
| } | |||
