Calculus of inductive constructions

From Wikipedia, the free encyclopedia

The introduction to this article provides insufficient context for those unfamiliar with the subject. Please help improve the article with a good introductory style.

This article does not cite any references or sources. (June 2008) Please help improve this article by adding citations to reliable sources. Unverifiable material may be challenged and removed.

The calculus of inductive constructions is the underlying core language of the Coq Proof Assistant. It is based on the calculus of constructions extended by inductive definitions as they are known from intuitionistic type theory.