4. Evolution
The Coq system, in its current state, is the result of over thirty years of research and attention to the needs of its users. A very slight knowledge of this evolution makes it possible to understand features that might seem complex or strange.
4.1 A tool born of fundamental research
Stemming from Thierry Coquand and Gérard Huet's work on Calcul des Constructions (CoC), themselves based on several decades of research in logic and fundamental and applied computer science, the first version of the Coq system, then called CONSTR, dates back to December 1984. A few experimental versions later, however, it was Thierry Coquand and Christine Paulin-Mohring's new Calcul des Constructions Inductives (CIC) that served as the foundation in 1989. The CONSTR system, based...
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
Evolution
Learn Rooster
Bibliography
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page. http://www.ocaml.org/...
Exclusive to subscribers. 97% yet to be discovered!
Already subscribed? Log in!
Article included in this offer
"Software technologies and System architectures"
(
234 articles
)
Updated and enriched with articles validated by our scientific committees
A set of exclusive tools to complement the resources
