Éditeur(s) :
HAL CCSD 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.
Second International Workshop on Proof Exchange for Theorem Proving (PXTP 2012)
Manchester, United Kingdom
hal-01126128
https://hal.archives-ouvertes.fr/hal-01126128