CoqInE: Translating the Calculus of Inductive Constructions into the -calculus Modulo

Second International Workshop on Proof Exchange for Theorem Proving

Mathieu Boespug1 ; Guillaume Burel2 ; 2 ENSIIE/Cedric/Inria AE Deducteam

Others  :  http://ceur-ws.org/Vol-878/paper3.pdf
PID  :  43472

来源: CEUR

【 摘 要 】

We show how to translate the Calculus of Inductive Constructions (CIC) as imple- mented by Coq into the -calculus modulo, a proposed common backend proof format