coq-pts

A formalisation of Pure Type Systems. This contrib is a formalization of Pure Type Systems. It includes most of the basic metatheoretical properties: weakening, substitution, subject-reduction, decidability of type-checking (for strongly normalizing PTSs). Strengtheningis not proven here. The kernel of a very simple proof checker is automatically generated from the proofs. A small interface allows interacting with this kernel, making up a standalone proof system. The Makefile has a special target "html" that produces html files from the sources and main.html that gives a short overview.

opam install coq-pts.8.5.0
homepage
https://github.com/coq-contribs/pts
license
Proprietary
bugs tracker
https://github.com/coq-contribs/pts/issues
dependencies
coq (>= 8.5 & < 8.6~)
source
https://github.com/coq-contribs/pts/archive/v8.5.0.tar.gz
package
https://github.com/coq/opam-coq-archive/tree/master/released/packages/coq-pts/coq-pts.8.5.0