Programmation certifiée avec Coq
Table of Contents
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
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"
- Algèbres et systèmes d'inférence (suite)
- 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"
- Algèbres et systèmes d'inférence (suite et fin)
- 7 février - 2*1h15
- Certification d'un tri par insertion
- Extraction de code
- 14 février - 2*1h15 - Evaluation
Introduction au cours - De l'efficacité surprenante de la logique en informatique
Les systèmes d'inférence
De la logique aux tactiques
- Praxis de la preuve en Coq
- Praxis = action en vue d'un but (d'un résultat pratique).
Types abstraits de données - Un point de vue algébrique
Coq : un guide
Software Foundations
Code à télécharger dans un même répertoire.
- Session 1 :
- cours : Basics - Functional Programming in Coq
- code : Basics - Functional Programming in Coq (premier rendu : le 9/01, 8h00 - travail en binôme)
- Session 2 :
- cours : The Curry-Howard Correspondence
- code : The Curry-Howard Correspondence
- Session 3 :
- cours : Proof by Induction
- code : Proof by Induction
- code requis : Basics (version longue de la session 1)
Evaluation
- Sujet : Exercices de programmation et de démonstration avec Coq
- Fichier à compléter :script