Calculus of (co)Inductive Constructions is a pure type system (Coquand, Huet) equipped with addition types: arbitrary (co)inductive types implementing general (co)inductive schemes; universes as a cumulative hierarchy of predicative types of types; and an impredicative type of propositions.
Related tags:
coq
|
created |
2 years, 10 months ago |
|
viewed |
11 times |
|
active |
2 years, 10 months ago |
|
editors |
1 |
