View source for Calculus of Inductive Constructions

The '''Calculus of Inductive Constructions''' (CIC) is the type-theoretic foundation of the [[Coq proof assistant|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