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.10.0.tar.gz
md5=191445dd2ce3ec6a10197be94dce4c05

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: 07 Dec 2019

Dependencies (2)

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

Dev Dependencies

None

Used by

None

Conflicts

None