Procedural Representation of CIC Proof Terms |
| |
Authors: | Ferruccio Guidi |
| |
Affiliation: | 1. Department of Computer Science, University of Bologna, Mura Anteo Zamboni 7, 40127, Bologna, Italy
|
| |
Abstract: | We propose an effective procedure, the first one to our knowledge, for translating a proof term of the Calculus of Inductive Constructions (CIC), into a tactical expression of the high-level specification language of a CIC-based proof assistant like coq (Coq development team 2008) or matita (Asperti et al., J Autom Reason 39:109–139, 2007). This procedure, which should not be considered definitive at its present stage, is intended for translating the logical representation of a proof coming from any source, i.e. from a digital library or from another proof development system, into an equivalent proof presented in the proof assistant’s editable high-level format. To testify to effectiveness of our procedure, we report on its implementation in matita and on the translation of a significant set of proofs (Guidi, ACM Trans Comput Log 2009) from their logical representation as coq 7.3.1 (Coq development team 2002) CIC proof terms to their high-level representation as tactical expressions of matita’s user interface language. |
| |
Keywords: | |
本文献已被 SpringerLink 等数据库收录! |
|