Declarative Representation of Proof Terms

10 years 5 months ago
Declarative Representation of Proof Terms
Abstract. We present a declarative language inspired by the pseudonatural language used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof terms. Then we investigate the relationship between the two translations, identifying the amount of proof structure preserved by compilation and re-generation of declarative scripts.
Claudio Sacerdoti Coen
Added 28 Jan 2011
Updated 28 Jan 2011
Type Journal
Year 2010
Where JAR
Authors Claudio Sacerdoti Coen
Comments (0)