URI http://ori.unit-c.fr/uid/unit-ori-wf-1-5283 Preuves de programmes en coq fre 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... 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 récursion fuscia LOMv1.0 hierarchical LOMv1.0 4 LOMFRv1.0 texte LOMv1.0 son LOMv1.0 image en mouvement LOMv1.0 ressource interactive LOMv1.0 final LOMv1.0 author BEGIN:VCARD VERSION:3.0 N:Bertot;Yves;;; FN:Yves Bertot EMAIL;TYPE=INTERNET:yves.bertot@inria.fr ORG:Inria END:VCARD 2012-09-21 LOMv1.0 publisher BEGIN:VCARD VERSION:3.0 N:Inria;;;; FN:Inria EMAIL;TYPE=INTERNET: ORG:Institut National de Recherche en Informatique et en Automatique END:VCARD 2012-09-21 LOMv1.0 publisher BEGIN:VCARD VERSION:3.0 N:UNIT;;;; FN:UNIT EMAIL;TYPE=INTERNET: ORG:UNIT END:VCARD 2012-09-21 URI http://ori.unit-c.fr/uid/unit-ori-wf-1-5284 LOMv1.0 validator BEGIN:VCARD VERSION:3.0 N:sduranton;Sylvain Duranton;;; FN:Sylvain Duranton sduranton ORG:Mon université URL:http://www.univ.fr UID:sduranton EMAIL;TYPE=INTERNET: END:VCARD LOMv1.0 creator BEGIN:VCARD VERSION:3.0 N:fuscia;fuscia;;; FN:fuscia fuscia ORG:Inria URL:http://www.univ.fr UID:fuscia EMAIL;TYPE=INTERNET: END:VCARD LOMv1.0 LOMFRv1.0 SupLOMFRv1.0 fre text/html video/mpeg http://www-sop.inria.fr/members/Yves.Bertot/videos-coq/ LOMv1.0 lecture LOMFRv1.0 outil LOMv1.0 exercise SupLOMFRv1.0 liste de références LOMv1.0 teacher LOMv1.0 learner LOMv1.0 higher education LOMFRv1.0 master SupLOMFRv1.0 bac+4 SupLOMFRv1.0 bac+5 LOMv1.0 very difficult P2DT12H 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. fre LOMv1.0 no LOMv1.0 yes 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 LOMv1.0 discipline Classification UNIT 1305 Programmation : Algorithmique, langages, conception objet, programmes CDD 22e éd. 005.11 Special programming techniques LOMv1.0 security level Projet OCW France tag-ocw Catalogue OCWC home-example unit-cofinance