Calculus of Constructions (CoC) is a dependent type system. It's on the lambda cube and is implemented in the Coq proof assistant.
Calculus of Constructions (CoC) is a dependent type system. It's on the lambda cube and is implemented in the Coq proof assistant.