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.

• Type: Journal
• Year: 2010
• Where: JAR
• Authors: Claudio Sacerdoti Coen
• Keywords: Declarative Language, Declarative Scripts, JAR 2010, Proof Terms