General Traits
The CoC is a higher-order typed lambda calculus, initially developed by Thierry Coquand, 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. Within Barendregt's lambda cube, it is therefore the richest calculus.
The CoC is strongly normalizing, although, by Gödel's incompleteness theorem, it is impossible to prove this property within the CoC since it implies consistency.
The CoC was the basis of the early versions of the Coq proof assistant; 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.
Read more about this topic: Calculus Of Constructions
Famous quotes containing the words general and/or traits:
“In communist society, where nobody has one exclusive sphere of activity but each can become accomplished in any branch he wishes, society regulates the general production and thus makes it possible for me to do one thing today and another tomorrow, to hunt in the morning, fish in the afternoon, rear cattle in the evening, criticize after dinner, just as I have a mind, without ever becoming hunter, fisherman, shepherd or critic.”
—Karl Marx (1818–1883)
“A child is born with the potential ability to learn Chinese or Swahili, play a kazoo, climb a tree, make a strudel or a birdhouse, take pleasure in finding the coordinates of a star. Genetic inheritance determines a child’s abilities and weaknesses. But those who raise a child call forth from that matrix the traits and talents they consider important.”
—Emilie Buchwald (20th century)