| Proof reflection in Coq (2002) | |||||||||||||||
Abstract | |||||||||||||||
| 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. 1 | |||||||||||||||
Details der Publikation | |||||||||||||||
| |||||||||||||||