GitHub - rocq-archive/prfx: Proof Reflection in Coq

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 20 Commits
Make		Make
Makefile		Makefile
ND.v		ND.v
ND_contr.v		ND_contr.v
ND_exch.v		ND_exch.v
ND_lift_lems.v		ND_lift_lems.v
ND_sound.v		ND_sound.v
ND_subst_lems.v		ND_subst_lems.v
ND_unique_types.v		ND_unique_types.v
README		README
check.v		check.v
check_sound.v		check_sound.v
contr.v		contr.v
description		description
eval.v		eval.v
eval_lift_lems.v		eval_lift_lems.v
eval_subst_lems.v		eval_subst_lems.v
exch.v		exch.v
indices.v		indices.v
inv_lems.v		inv_lems.v
lift.v		lift.v
lift_lems.v		lift_lems.v
list.v		list.v
nat_eqb.v		nat_eqb.v
objects.v		objects.v
prfx.v		prfx.v
prfx_tree.dot		prfx_tree.dot
red.v		red.v
subj_red.v		subj_red.v
subst.v		subst.v
subst_lems.v		subst_lems.v
thesis.bib		thesis.bib
thesis.pdf		thesis.pdf
thesis.ps		thesis.ps

Repository files navigation

title:      Proof Reflection in Coq
author:     Dimitri Hendriks, <[email protected]>
version:    Coq 8.0pl1
date:       completed: 20030831;  contrib.: 20050415
www:        <http://www.cs.ru.nl/~hendriks/coq/prfx/>
doc.:       Ch. 2 of Hendriks' PhD thesis (thesis.*)
compile:    make opt
dep. graph: dotty prfx_tree.dot
abstract:

  Natural deduction for first-order logic is formalised 
  in the proof assistant Coq, using De Bruijn indices 
  for variable binding. The main judgement is of the 
  form G |- d [:] p, stating that d is a proof term of 
  formula p under hypotheses G; 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, I define a 
  reduction relation on proof terms with permutative 
  conversions and prove the property of subject reduction.