Sciweavers

JAR
2002

Proof Reflection in Coq

13 years 10 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 [:] , stating that d is a proof term of formula under hypotheses ; it can be viewed as a typing relation by the Curry-Howard isomorphism. This relation is proved sound with respect to Coq's native logic and is amenable to the manipulation of formulas and of derivations. As an illustration, we define a reduction relation on proof terms with permutative conversions and prove the property of subject reduction.
Dimitri Hendriks
Added 22 Dec 2010
Updated 22 Dec 2010
Type Journal
Year 2002
Where JAR
Authors Dimitri Hendriks
Comments (0)