Calculus of inductive constructions
From Wikipedia, the free encyclopedia
 |
This article provides insufficient context for those unfamiliar with the subject. Please help improve the article with a good introductory style. (October 2009) |
 |
This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (June 2008) |
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.
[edit] See also
[edit] References
http://coq.inria.fr/doc/Reference-Manual006.html
 |
This programming language theory or type theory-related article is a stub. You can help Wikipedia by expanding it. |
