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...
The Ultimate Scientific and Technical Reference
This article is included in
Software technologies and System architectures
This offer includes:
Knowledge Base
Updated and enriched with articles validated by our scientific committees
Services
A set of exclusive tools to complement the resources
Practical Path
Operational and didactic, to guarantee the acquisition of transversal skills
Doc & Quiz
Interactive articles with quizzes, for constructive reading
Evolution
Learn Rooster
Bibliography
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page. http://www.ocaml.org/...
The Ultimate Scientific and Technical Reference
