Procedural Representation of CIC Proof Terms

Abstract. In this paper we propose an effective procedure for translating a proof term of the Calculus of Inductive Constructions (CIC), which is very similar to a program written in a prototypal functional programming language, into a tactical expression of the high-level specification language of a CIC-based proof assistant like coq [1] or matita [2]. As a use case, we report on our implementation of this procedure in matita and on the translation of 668 proofs generated by coq 7.3.1 [3]1 , from their logical representation as CIC proof terms to their high-level representation as tactical expressions of matita’s user interface language.

• Type: Journal
• Year: 2010
• Where: JAR
• Authors: Ferruccio Guidi
• Keywords: CIC-based Proof Assistant, Functional Programming Language, JAR 2010, Tactical Expressions