Formation Coq pour l'industrie

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.

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

Public :

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. 

Introduction

Le langage fonctionnel

Le langage de preuves

Cas pratiques

Les travaux pratiques représentent 50% du temps de formation.