- Durée
- 3 jours
- Niveau
- Intermédiaire
- Modalités
- Distanciel
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.
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
Objectifs opérationnels
Savoir structurer un développement et faire des preuves en Coq.
Programme
Contenu du cours, module par module
4 modules
- Présentation de Coq
- Domaines d'application
- Écosystème
- Installation et premiers pas
- Le calcul des constructions
- Définitions et commandes
- Arguments implicites
- Sections
- Modules
- Notations
- Documentation
Travaux pratiques
- Définition des propriétés
- Tactiques de base
- Tactiques évoluées
- Le langage Ltac
- L'isomorphisme de Curry-Howard
Travaux pratiques
- Un mini langage
- Une politique de contrôle d'accès
Travaux pratiques
Les travaux pratiques représentent 50% du temps de formation.
Programme mis à jour le 18/03/2024
Public concerné
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.
Faire le testFinancement
Cette formation peut être prise en charge par votre entreprise, seule ou avec l’appui de son opérateur de compétences. Nous fournissons le devis et les pièces attendues par l’OPCO.
Formations liées
- CUDA - InitiationRéf. CUDA1 jourFondamental
- CUDA - Prise en mainRéf. CUDO3 joursIntermédiaire
- Dask : mise en œuvre de la programmation parallèle en PythonRéf. DASK3 joursIntermédiaireProchaine session : 21 déc.2 550 €
- Data Visualisation en PythonRéf. OPDV3 joursIntermédiaireProchaine session : 21 oct.2 090 €