Calculus of Inductive Constructions

The Calculus of Inductive Constructions (CIC) is the type-theoretic foundation of the Coq proof assistant and one of the most expressive constructive logics ever developed. It extends the pure Calculus of Constructions with inductive definitions — the ability to declare data types and predicates by their constructors and to reason about them by structural induction — creating a unified framework in which programs, specifications, and proofs are the same species of object. The CIC is not a programming language with a logic attached, nor a logic with a programming language attached; it is a single system in which the distinction between computation and reasoning has been erased by design.

The constructive discipline of the CIC is its most consequential feature: every proof of existence must be a witness, every function must be computable, and every proposition is a type whose inhabitants are the proofs of that proposition. This is the formal realization of the Brouwer-Heyting-Kolmogorov interpretation of intuitionistic logic, and it is the reason that Coq-extracted programs are not merely correct