Ressource pédagogique : Preuves de programmes en coq

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 ...
cours / présentation, outil, exercice, liste de références - Date de création : 21-09-2012
Auteur(s) : Yves Bertot
Partagez !

Présentation de: Preuves de programmes en coq

Informations pratiques sur cette ressource

Français
Type pédagogique : cours / présentation, outil, exercice, liste de références
Durée d'apprentissage : 2 jours 12 heures
Niveau : enseignement supérieur, master, bac+4, bac+5
Langue de l'apprenant : Français
Contenu : texte, son, image en mouvement, ressource interactive
Public(s) cible(s) : enseignant, apprenant
Document : Document HTML, Vidéo MPEG
Difficulté : très difficile
Droits : pas libre de droits, gratuit
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

Description de la ressource pédagogique

Description (résumé)

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

  • Granularité : module
  • Structure : hiérarchique

"Domaine(s)" et indice(s) Dewey

  • Special programming techniques (005.11)

Thème(s)

Informations pédagogiques

  • 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.

Intervenants, édition et diffusion

Intervenants

Créateur(s) de la métadonnée : fuscia fuscia
Validateur(s) de la métadonnée : Sylvain Duranton sduranton

Editeur(s)

Diffusion

Partagez !

AUTEUR(S)

  • Yves Bertot
    Inria

ÉDITION

Inria

UNIT

EN SAVOIR PLUS

  • Identifiant de la fiche
    http://ori.unit-c.fr/uid/unit-ori-wf-1-5283
  • Identifiant
    unit-ori-wf-1-5283
  • Statut de la fiche
    final
  • Schéma de la métadonnée
  • Entrepôt d'origine
    UNIT
  • Date de publication
    21-09-2012