Preuves de programmes en coq

Auteur(s) : BERTOT YVES 21-09-2012
Éditeur(s) : Inria Institut National de Recherche en Informatique et en Automatique, UNIT UNIT;

Description : 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...

Mots-clés libres : Coq, assistant de preuve, programmation fonctionnelle sûre, preuve de programme, logique mathématique, méthode formelle, calcul des constructions, correction de logiciel, algorithmique certifiée, théorie des types, logiciel libre, récursion, fuscia
Classification générale : Informatique

Accès à la ressource : http://www-sop.inria.fr/members/Yves.Bertot/videos...
Etat d'achèvement : final
Conditions d'utilisation : Ces ressources de cours sont la copropriété, à parts égales, d’UNIT et de l'Inria et relèvent de la licence logicielle GPL, dans sa version française CeCILL : http://www.cecill.info/licences/Licence_CeCILL-V1_VF.pdf

DONNEES PEDAGOGIQUES

Type pédagogique : cours / présentation, outil, exercice, liste de références
Granularité : module
Niveau : enseignement supérieur, master, bac+4, bac+5
Public cible : enseignant, apprenant

Langue de l'apprenant : Français

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.

Difficulté : très difficile

Durée d'apprentissage : 2 jours 12 heures

DONNEES TECHNIQUES

Format : text/html, video/mpeg

Exporter au format XML