Programmation certifiée avec Coq

Installation
Agenda - Liens vers les TP
Introduction au cours - De l'efficacité surprenante de la logique en informatique
Les systèmes d'inférence
Logiques
De la logique aux tactiques
Types abstraits de données - Un point de vue algébrique
Coq : un guide
Software Foundations
Evaluation

Ce cours s'adresse aux élèves de seconde année en apprentissage, recrutés après une formation initiale universitaire de deux ans consacrée à l'informatique. Le volume horaire est d'une quinzaine d'heures.

L'objectif du cours est l'apprentissage de la programmation certifiée,

en utilisant Coq,
en s'appuyant sur les correspondances existant entre la logique et la programmation.

Installation

Instructions

Agenda - Liens vers les TP

6 janvier - 1h15
- Introduction
- Les systèmes d'inférence
9 janvier - 1h15
- Les systèmes d'inférence (suite)
- Logique
- TP 1 + correction Tuto 1
16 janvier - 1h15
- Logique (suite) - Premier ordre, ordre supérieur
- Correspondance de Curry-Howard
24 janvier - 1h15
- Systèmes d'inférence paramétrés et indexés
- Du calcul des séquents aux tactiques
- Exemple : les nombres binaires (TP2, Binaire.v dans le dépôt) - Style "preuve"
27 janvier - 1h15
- Exemple (suite) : les nombres binaires (TP2, Binaire.v dans le dépôt) - Style "preuve"
30 janvier - 1h15
- Tactiques liées à l'égalité et aux contradictions
- Algèbres et systèmes d'inférence
  - Initialité
  - Quotient
- Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
3 février - 1h15
- Algèbres et systèmes d'inférence (suite)
  - Initialité
  - Quotient
- Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
4 février - 1h15
- Algèbres et systèmes d'inférence (suite et fin)
  - Initialité
  - Quotient
- Exemple : les nombres bianires (TP3, tp3.v dans le dépôt) - Style "preuve"
7 février - 2*1h15
- Certification d'un tri par insertion
- Extraction de code
14 février - 2*1h15 - Evaluation