Sciweavers

Share
JAR
2010
160views more  JAR 2010»
9 years 7 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 t...
Claudio Sacerdoti Coen
JAR
2002
77views more  JAR 2002»
9 years 9 months ago
Proof Reflection in Coq
We formalise natural deduction for first-order logic in the proof assistant Coq, using De Bruijn indices for variable binding. The main judgement we model is of the form d [:] , ...
Dimitri Hendriks
TPHOL
2000
IEEE
10 years 1 months ago
Proof Terms for Simply Typed Higher Order Logic
Abstract. This paper presents proof terms for simply typed, intuitionistic higher order logic, a popular logical framework. Uniļ¬cation-based algorithms for the compression and re...
Stefan Berghofer, Tobias Nipkow
books