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>
  2. H
    Hugo Herbelin <hugo.herbelin@inria.fr>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=4ba0c590baf4df955e3440ca456440ce

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.

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: 07 Jun 2016

Dependencies (2)

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

Dev Dependencies

None

Used by (1)

  1. coq-ptsf < "8.6.0"

Conflicts

None