indiquent une
vidéo de démonstration d'utilisation de Coq, qui complémente le cours principal.
Ce cours vidéo a été préparé en 2009 par Yves Bertot avec l'aide de Patrick Rambert et quelques collègues assemblés par Patrick.
Si les liens vers des vidéos sont cassés, prévenez Yves Bertot et essayez la page suivante.
Le cours est décomposé en 7 parties. Des liens vers des archives compressées pour chaque partie sont disponibles : partie 1, 2, 3, 4, 5, 6, 7.
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, ...
Ce cours vidéo s'adresse à un public informaticien avec des prérequis qui sont partagés par la majeure partie des ingénieurs du milieu industriel.
Les pictogrammes comme celui-ci indiquent une
vidéo de démonstration d'utilisation de Coq, qui complémente le cours principal.