5. Apprendre Coq
Les plus de cinq cents pages du manuel de référence de Coq ne doivent pas effrayer le futur utilisateur. Coq se doit d’être un logiciel très complet, où de nombreux outils assistent l’utilisateur dans le développement de démonstrations correctes. Quelques jours suffisent pour être capable de prouver la correction de petits programmes fonctionnels simples comme la fonction de tri donnée en exemple dans cet article. Cet apprentissage peut se faire en travaillant sur les nombreux tutoriaux ou ouvrages plus complets
Cet article est réservé aux abonnés. Il vous reste 92 % à découvrir.
Déjà abonné ? Se connecter
Apprendre Coq
Conclusion
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.
