# Calculus of Constructions

> In mathematical logic and computer science, the calculus of constructions (CoC) is a type theory created by Thierry Coquand. It can serve as both a typed programming language and as constructive foundation for mathematics.

In <mathematical logic> and [computer science](https://wiki.g15e.com/pages/Computer%20science.txt), the calculus of constructions (CoC) is a [type theory](https://wiki.g15e.com/pages/Type%20theory.txt) created by <Thierry Coquand>. It can serve as both a typed programming language and as constructive foundation for mathematics.

## Implementations

- [Lean](https://wiki.g15e.com/pages/Lean%20(programming%20language.txt))