4. Évolution
Le système Coq, dans son état actuel, est le résultat de plus de trente ans de recherches et d’attention aux besoins de ses utilisateurs. Une connaissance très légère de cette évolution permet de comprendre des caractéristiques qui pourraient paraître complexes ou étranges.
4.1 Outil issu de la recherche fondamentale
Issue des travaux de Thierry Coquand et Gérard Huet sur le Calcul des Constructions (en anglais CoC), eux-mêmes s’appuyant sur plusieurs décennies de recherche en logique et en informatique fondamentale et appliquée, la première version du système Coq, alors appelée CONSTR, date de décembre 1984. Quelques versions expérimentales plus tard, ce sera cependant le nouveau Calcul des Constructions Inductives (en anglais CIC) de Thierry Coquand et...
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Évolution
Apprendre Coq
Sources bibliographiques
- (1) - - The CompCert compiler. http://compcert.inria.fr .
- (2) - - OCaml page.
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Article inclus dans l'offre
"Technologies logicielles Architectures des systèmes"
(
408 articles
)
Actualisée et enrichie d’articles validés par nos comités scientifiques.
Quiz, médias, tableaux, formules, vidéos, etc.
Opérationnels et didactiques, pour garantir l'acquisition des compétences transverses.
Un ensemble de services exclusifs en complément des ressources.
