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 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

Introduction

  • Présentation de Coq
  • Domaines d'application
  • Écosystème
  • Installation et premiers pas

Le langage fonctionnel

  • Le calcul des constructions
  • Définitions et commandes
  • Arguments implicites
  • Sections
  • Modules
  • Notations
Travaux pratiques : découverte de la bibliothèque standard, écriture de programmes simples et leur évaluation.

Le langage de preuves

  • Définition des propriétés
  • Tactiques de base
  • Tactiques évoluées
  • Le langage Ltac
  • L'isomorphisme de Curry-Howard
Travaux pratiques: spécification et preuve des programmes précédemment écrits

Cas pratiques

  • Un mini langage arithmétique
  • Une politique de contrôle d'accès

Coq pour l'industrie

Durée: 3 jours Prix: 2500 EUR HT/pers Pratique: 50%
Prérequis
  • Algorithmique
  • Prog. Fonctionnelle
  • Mathématiques
Public
  • Développeurs
Objectifs Pédagogiques
  • Introduction
  • Le langage fonctionnel
  • Le langage de preuves
  • Cas pratiques

Julien Blond (Coq)

Julien est ingénieur R&D chez OCamlPro depuis 2021, après une thèse de doctorat et une longue expérience dans l'industrie. Julien est un développeur OCaml aguérri, mais aussi un expert des méthodes formelles, et en particulier de la vérification et de la certification en utilisant l'assistant de preuve Coq, par exemple pour les Critères Communs en cyber-sécurité.

Évaluation des acquis

L'évaluation des acquis de la formation se fera en séance au travers d'ateliers, d'exercices et/ou de travaux pratiques. Dans le cas d'une formation officielle éditeur, veuillez nous consulter afin que nous vous fassions part des modalités d'évaluation.

A l'issue de la formation, vous sera transmis une évaluation à chaud de l'action de formation qui vous permettra de nous faire part de vos retours quant à votre expérience apprenant avec OCamlPro.

Prise en compte RQTH

Si vous êtes sujet à un handicap, prenez contact avec nos équipes pour que nous puissions définir ensemble comment nous pourrons aménager la session afin que vous puissiez vivre une expérience en formation inchangée.

Ressources pédagogiques

Les ressources pédagogiques sont produites par l'équipes OCamlPro en vue des formations. Les documents sont généralement en anglais, mais peuvent être traduits en français à la demande.

Financement en France

Nos formations ne sont pas éligibles au financement via OPCO (même si la prise en charge couvre la totalité du coût de la formation) en attendant la certification Qualiopi en cours. Non éligible au financement via CPF.

Formation en inter-entreprises

Les horaires pour nos formations inter-entreprises in-situ sont :

  • Début de la formation - 9h30
  • Pause déjeuner - 12h à 13h
  • Fin de la formation - 17h30