package coq-ptsf
Explicit Convertibility Proofs in Pure Type Systems
Install
Dune Dependency
Authors
Maintainers
Sources
v8.8.0.tar.gz
md5=dd82b98b28be2cf0a46a8d6316397064
Description
http://www.andrew.cmu.edu/user/fpv/ptsf/
Formalization of the proof that PTS and PTS with explicit convertibility proofs (PTSf) are equivalent.
Tags
keyword: pure type systems keyword: judgmental equality keyword: explicit equality proofs keyword: proof relevance category: Mathematics/Logic/Type theoryPublished: 06 Feb 2019
Dependencies (3)
-
coq-ptsatr
>= "8.8" & < "8.9~" -
coq
>= "8.8" & < "8.9~" - ocaml
Dev Dependencies
None
Used by
None
Conflicts
None
On This Page