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.7.0.tar.gz
md5=b77b1bc10c081e5fce0ce9fb46e7a661

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: 11 Jan 2019

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None