Preuves de programmes en coq
Bertot Yves
Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique d'ordre supérieur. Tous ces aspects reposent sur l'utilisation avancée de la notion de typage et sur les relations intimes entre types, spécifications, et calculs. L'auteur Yves Bertot est chercheur à l'INRIA et travaille avec le système depuis une vingtaine d'années. Il a utilisé ce système pour des études d'algorithmes en technologie des langages de programmation, géométrie, arithmétique des ordinateurs...Description
Université productrice
Université numérique ingénierie et technologie, Institut national de recherche en informatique et en automatique
Discipline
Informatique - Programmation : Algorithmique, langages, conception objet, programmes
Mots clés
fuscia, Coq, preuve de programme, méthode formelle, logique mathématique, logiciel libre, assistant de preuve, programmation fonctionnelle sûre, calcul des constructions, correction de logiciel, algorithmique certifiée, théorie des types, récursion
Langues
Français
Droits attachés à la ressource
Licence CeCILL version 2
Indication pédagogique
Niveaux
M1, M2, Master
Proposition d'utilisation
Ce cours vidéo pour se former au langage Coq s'adresse à un public informaticien avec des prérequis qui sont partagés par la majeure partie des ingénieurs du milieu industriel.
Type(s) pédagogique(s)
Cours / Présentation, Liste de références, Outil, Exercice
Type(s) documentaire(s)
Texte, Son, Vidéo, Ressource interactive
Durée d'apprentissage
60h00m00s