Science Fair Project Encyclopedia
Calculus of Constructions
(Redirected from Calculus of constructions)
The Calculus of Constructions (CoC) is a higher-order typed lambda calculus where types are first-class values. It is thus possible, within the CoC, to define functions from, say, integers to types, types to types as well as functions from integers to integers. The CoC is strongly normalizing .
The CoC was initially developed by Thierry Coquand .
The CoC was the basis of the early versions of the Coq theorem prover; later versions were built upon the Calculus of Inductive Constructions an extension of CoC with native support for inductive datatypes. In the original CoC, inductive datatypes had to be emulated as their polymorphic destructor function.
10-26-2009 08:16:03
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details
The contents of this article is licensed from www.wikipedia.org under the GNU Free Documentation License. Click here to see the transparent copy and copyright details