package coq-pts

  1. Overview
  2. No Docs
A formalisation of Pure Type Systems

Install

Dune Dependency

Authors

Maintainers

Sources

v8.6.0.tar.gz
md5=17d9aa978a4164823cacbb737f104f40

Description

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.

Dependencies (2)

  1. coq >= "8.6" & < "8.7~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None