initially developed by Thierry Coquand. It is well known for being at the top of Barendregt's lambda cube. It is possible within CoC to define functions from terms to terms, terms to types, types to types, and from types to terms.

The CoC is strongly normalizing, and hence consistent.

Usage

The

1.Previous
3.Next