GitHub - rocq-archive/ptsatr: Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.

rocq-archive / ptsatr Public

Notifications You must be signed in to change notification settings
Fork 0
Star 2

Formalization of the proof that PTS and PTS with judgmental equality (PTSe) are equivalent. With this equivalence, we are able to derive all the meta-theory of PTSe, like Pi-injectivity or Subject Reduction.

2 stars 0 forks Branches Tags Activity

Star

Notifications

Branches Tags

Name		Name	Last commit message	Last commit date
Latest commit History 16 Commits
Make		Make
Makefile		Makefile
README		README
base.v		base.v
counter_ex.v		counter_ex.v
description		description
env.v		env.v
final_result.v		final_result.v
glue.v		glue.v
red.v		red.v
strip.v		strip.v
term.v		term.v
typ_annot.v		typ_annot.v
ut_env.v		ut_env.v
ut_red.v		ut_red.v
ut_sr.v		ut_sr.v
ut_strengh.v		ut_strengh.v
ut_term.v		ut_term.v
ut_typ.v		ut_typ.v
ut_typ_eq.v		ut_typ_eq.v
ut_typ_eq_inj.v		ut_typ_eq_inj.v

Repository files navigation

Author: Vincent Siles <vincent.siles@ens-lyon.org>
        Hugo Herbelin <hugo.herbelin@inria.fr>

Formalization of the proof that PTS and PTSe are equivalent.
Tested with Coq 8.3

INSTALL:
use "coq_makefile -f Make" to compile