You are viewing the staging branch of the website @ 58d46ed, not the live version.

package coq-ptsatr

Overview
Homepage

You can search for identifiers within the package.

in-package search v0.2.0

PTSATR

Install

Dune Dependency

www.lix.polytechnique.fr Edit opam file Versions (6)

Authors

V

Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles]
H

Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]

Maintainers

H

Hugo.Herbelin@inria.fr

Sources

v8.10.0.tar.gz

md5=88109005908fca0aeff7afac0b568d1e

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.

Published: 07 Dec 2019

Dependencies (2)

coq >= "8.10" & < "8.11~"
ocaml

Dev Dependencies

None

Used by (1)

coq-ptsf >= "8.10.0"

Conflicts