Calculus of Constructions
- 2025-09-14
- 별칭: CoC
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.