Procedural Representation of CIC Proof Terms

9 years 7 months ago
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.
Ferruccio Guidi
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JAR
Authors Ferruccio Guidi
Comments (0)