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

Program

(to be translated soon...)

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

Industrial Coq

Duration: 3 days Practice: 50%
Price: 2500 EUR/person excl. taxes
Pre-requisites
  • Algorithmique
  • Prog. Fonctionnelle
  • Mathématiques
Public
  • Développeurs
Pedagological Objectives
  • (to be translated soon...)
  • 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é.

Evaluating progress

We make the progress of our trainees and its evaluation a core aspect of our courses. Indeed, guaranteeing the durable acquisition of the skills at hand is key, especially for the newer comers. To that extent, we will have trainees undergo tailored group works, exercises and hands-on practice which modalities can all be customised to your specific needs.

At the end of the course, you will have an opportunity for feedback to help us improve upon our methods. This is crucial as we believe there is always room for learning on both sides of the desk and no opinion other than yours matters more for us to do so.

Considering RQTH(Recognition of Handicapped Worker Status)

If people with disabilities are part of the course, do reach out to us so we can adapt the training accordingly.

Pedagogical Ressources

The ressources are written by the OCamlPro team prior to the courses. Documents are generally written in english and can be translated to french if need be.

Funding resorts in France

Unfortunately our trainings cannot yet be funded by institutions such as OCPO (despite these funds fully covering the price of our trainings), neither can they be funded by CPF.

Inter Corporation Trainings

Time slots for our on-site Inter Corporation Trainings are the following:

  • Start - 9:30AM
  • Lunch Break - 12:00PM to 01:00PM
  • End - 05:30PM