Ruby On Rails
- Durée
- Durée :4 jours
- Niveau
- Niveau :Intermédiaire
- Certification
- Certification :Non
Intra uniquement
Aucune session prévue
Coq pour l'industrie
Description de la formation Coq
L'assistant de preuve Coq est un outil de développement formel utilisé dans le cadre académique mais également industriel pour modéliser ou vérifier des programmes.
Cette formation Coq, de trois jours, orientée vers l'industrie, permet d'initier les apprenants au langage et son écosystème ainsi qu'au développement et à la preuve de programme en utilisant des techniques simples.
Programme de la formation
Objectif opérationnel :
Savoir structurer un développement et faire des preuves en Coq.
Objectifs pédagogiques :
À l'issue de cette formation Coq vous aurez acquis les connaissances et les compétences nécessaires pour :
- Installer Coq
- Programmer en Coq
- Structurer un développement Coq
- Faire des preuves en Coq
- Extraire des programmes
- Produire du matériel certifiable
Introduction
Présentation de CoqDomaines d'application
Écosystème
Installation et premiers pas
Le langage fonctionnel
Le calcul des constructionsDéfinitions et commandes
Arguments implicites
Sections
Modules
Notations
DocumentationTravaux pratiquesDécouverte de la bibliothèque standard, écriture de programmes simples et leur évaluation
Le langage de preuves
Définition des propriétésTactiques de base
Tactiques évoluées
Le langage Ltac
L'isomorphisme de Curry-HowardTravaux pratiquesSpécification et preuve des programmes précédemment écrits
Cas pratiques
Un mini langageUne politique de contrôle d'accès
Public cible :
Ce cours Coq s'adresse principalement aux développeurs.
Prérequis :
Pour suivre cette formation Coq il est nécessaire d'avoir de bonnes connaissances en algorithmique, en programmation fonctionnelle ainsi qu'en mathématiques.
J'évalue mes connaissances pour vérifier que je dispose des prérequis nécessaires pour profiter pleinement de cette formation en faisant le test de prérequis.
Date de mise à jour du programme : 18/03/2024