Calculus of inductive construction

Tools: Rocq (formerly Coq)

• (Formal system, Logic, Computation theory) A type theory combining Dependent types, Inductive types, and a hierarchy of universes, serving as the theoretical foundation of Coq.