package coq-ptsatr

  1. Overview
  2. No Docs
PTSATR

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. V
    Vincent Siles <vincent.siles@ens-lyon.org> [http://www.lix.polytechnique.fr/~vsiles]
  2. H
    Hugo Herbelin <hugo.herbelin@inria.fr> [http://pauillac.inria.fr/~herbelin/]

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.7.0.tar.gz
md5=16d1f7d21ab36e2ebc2c327a52274c32

Description

http://www.lix.polytechnique.fr/~vsiles/coq/PTSATR.html

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.

Tags

keyword: pure type systems keyword: judgmental equality keyword: Church-Rosser keyword: confluence keyword: subject reduction keyword: pi injectivity category: Mathematics/Logic/Type theory

Published: 11 Jan 2019

Dependencies (2)

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

Dev Dependencies

None

Used by (1)

  1. coq-ptsf = "8.7.0"

Conflicts

None