3 ms·
It's also, IIRC, based on a logical model called the Calculus of Constructions - or CoC, for short.
by wk_end 12y ago
It's also, IIRC, based on a logical model called the Calculus of Constructions - or CoC, for short.
- bch 12y ago> It's also, IIRC, based on a logical model called the Calculus of Constructions "Calculus of Inductive Constructions" (https://coq.inria.fr/about-coq https://coq.inria.fr/about-coq)
- Cederfjard 12y agoFrom your link: > Coq is the result of more than 20 years of research. It started in 1984 from an implementation of the Calculus of Constructions at INRIA-Rocquencourt by Thierry Coquand and Gérard Huet. In 1991, Christine Paulin extended it to the Calculus of Inductive Constructions.
- tel 12y agoThe CoC provides the basic framework for Coq, while the Co(I)C or even the Calculus of (Co)-Inductive Constructions provides a dramatic extension in power and expressivity necessary for "real" programming in Coq.