package coq-ptsf

  1. Overview
  2. No Docs
Explicit Convertibility Proofs in Pure Type Systems

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. H
    Herman Geuvers <herman@cs.ru.nl>
  2. F
    Floris van Doorn <fpv@andrew.cmu.edu>
  3. F
    Freek Wiedijk <freek@cs.ru.nl>

Maintainers

  1. M
    matej.kosik@inria.fr

Sources

v8.5.0.tar.gz
md5=29e7294dfdd89c6e120b3b812938ad20

Description

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 theory

Published: 07 Jun 2016

Dependencies (3)

  1. coq-ptsatr = "8.5.0"
  2. coq >= "8.5" & < "8.6~"
  3. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None