Sommaire
cours / présentation, outil, exercice, liste de références
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 ...
Date de création :
21.09.2012Auteur(s) :
Yves BertotAccéder à la ressource :
Présentation
Informations pratiques
Langue du document : Français
Type : cours / présentation, outil, exercice, liste de références
Temps d'apprentissage : 2 jours 12 heures
Niveau : enseignement supérieur, master, bac+4, bac+5
Langues : Français
Contenu : texte, son, vidéo, ressource interactive
Public(s) cible(s) : enseignant, apprenant
Document : Document HTML, Vidéo MPEG
Difficulté : très difficile
Droits d'auteur : 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
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
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)
Domaine(s)
- Informatique
- Programmation : Algorithmique, langages, conception objet, programmes
- Informatique
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
Édition
- Inria
- UNIT
Diffusion
Cette ressource vous est proposée par :
Fiche technique
Identifiant de la fiche : http://ori.unit-c.fr/uid/unit-ori-wf-1-5283
Identifiant OAI-PMH : oai:www.unit.eu:unit-ori-wf-1-5283
Statut de la fiche : final
Schéma de la métadonnée : oai:uved:Cemagref-Marine-Protected-Areas
- LOMv1.0
- LOMFRv1.0
- SupLOMFRv1.0
- Voir la fiche XML
Entrepôt d'origine : UNIT
Voir aussi
01.08.2011
Description
:
Les ordinateurs ne savent pas prouver seuls des théorèmes profonds. Cependant, grâce aux assistants de preuve, ils garantissent les démonstrations découvertes par les mathématiciens.
- assistant de preuve
- preuve formelle
- preuve de programme
- logique mathématique
- démonstration
- complexité
- fuscia
11.12.2008
Description
:
Peut-on être sûr de la vérité d’une preuve ? Cette preuve de la preuve, comment l’obtenir en pratique ? La vérification formelle de démonstration est de plus en plus utilisée par les mathématiciens.
- preuve de programme
- preuve formelle
- logique mathématique
- démonstration
- Coq
- théorème des quatre couleurs
- fuscia