fuscia.info
Preuves de programmes en coq - Yves Bertot - INRIA

 
cours Preuves en coq

Programmation récursive

4.1 - Les types dépendants - 7:25

4.2 - Le polymorphisme - 3:24  

4.3 - Fonctions à types dépendants - 10:25

4.4 - Les propositions sont des types - 5:56

4.5 - Construction de preuves - 7:27

4.6 - Filtrage et récursion dépendants - 12:57

4.7 - Types récursifs dépendants - 8:37

4.8 - Propositions inductives - 10:05

Prédicats inductifs

5.1 - Familles de types récursifs - 8:13

5.2 - Familles de types récursifs hétérogènes - 13:17  

5.3 - Principes de récurrence pour les prédicats inductifs - 8:04  

5.4 - Présentation inductive de concepts usuels - 8:44

Types pour les spécifications

6.1 - Valeurs certifiées - 10:54  

6.2 - Programmation par preuve - 9:55

6.3 - Exemple de programmation avec valeurs certifiées - 11:24

6.4 - Extraction - 11:31

Récursion générale

7.1 - Récursion générale - 12:04  

7.2 - Relations bien fondées - 5:20  

7.3 - La commande Function - 10:20    

7.4 - La notion d'accessibilité - 7:04



Utilisation de coq

... pour l'étude d'algorithmes - 8:42

... pour l'étude des langages de programmation - 13:10

... pour les mathématiques - 7:17


Introduction ...

1.1 - Les fonctions en Coq - 5:04  

1.2 - Jouer avec les fonctions - 7:20

1.3 - Les types en Coq - 8:17

1.4 - Le polymorphisme - 6:29

1.5 - L'ordre supérieur - 2:13      

1.6 - Les structures de données en Coq - 1:37    

1.7 - Manipulation des couples - 3:52

1.8 - Types inductifs en Coq - 7:45  

1.9 - Fonctions récursives - 8:40

1.10 - Bibliothèque de base - 5:34

1.11 - Nombres naturels et récursion - 2:51  

1.12 - Valeurs boolénnes, couples et listes - 5:28  

1.13 - Polymorphisme - 12:55

Interprétation du type

2.1 - Les formules logiques en coq - 7:33

2.2 - Faire des preuves en coq - 11:19  

2.3 - Preuves avec les connecteurs logiques - 10:50    

2.4 - Outils avancés pour les preuves - 10:15

2.5 - Structuration des preuves - 3:48

2.6 - Premières preuves de programmes - 7:50  

2.7 - Egalités - 5:10

Types dépendants

3.1 - Introduction aux propriétés inductives en Coq - 11:45  

3.2 - Approche inductive des connecteurs logiques - 11:41

3.3 - Principes de récurrences de propriétés en Coq - 9:50

3.4 - Inversion des propriétés inductives - 8:31