Contribution: PTSATR

PTSATR

Authors

Description

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.

Keywords

pure type systems, judgmental equality, chruch rosser, confluence, subject reduction, pi injectivity

README

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

Available files