package coq-historical-examples

  1. Overview
  2. No Docs
Historical examples developed in the (pure) Calculus of Constructions

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. G
    Gérard Huet
  2. C
    Christine Paulin

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.9.0.tar.gz
md5=f85e8849d299c1fbdb2e8a34d8a63cc3

Description

This is a collection of historical examples developed in system CoC that implemented Coquand's Calculus of Constructions. Newman.v and Tarski.v originate in version 1.10, Manna.v and Format.v are from version 4.3. Their evolution to the Calculus of Inductive Constructions (up to Coq V6.3) are in MannaCIC.v and FormatCIC.v. (Collection by Hugo Herbelin.)

Tags

keyword: Newman's lemma keyword: Tarski's fixpoint theorem keyword: line formatting keyword: binary-search paradigm keyword: square root approximation keyword: Calculus of Constructions keyword: history of Coq category: Miscellaneous/Coq Use Examples

Published: 08 Dec 2019

Dependencies (2)

  1. coq >= "8.9" & < "8.10~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None