Cours Vidéo de Coq

Ce cours vidéo a été préparé en 2009 par Yves Bertot avec l'aide de Patrick Rambert et quelques collègues assemblés par Patrick. Le site web initial contenait des outils javascript pour améliorer la présentation des données, mais ce site a été désactivé au début début de l'année 2017. Cette est une tentative minimaliste pour redonner accès au contenu.

Si les liens vers des vidéos sont cassés, prévenez Yves Bertot et essayez la page suivante.

Le cours est décomposé en 7 parties. Des liens vers des archives compressées pour chaque partie sont disponibles : partie 1, 2, 3, 4, 5, 6, 7.

Introduction

Le système Coq fournit un langage de programmation symbolique et un cadre logique pour raisonner sur les algorithmes décrits. 

Dans ce cours, nous décrivons les points clefs du langage de programmation, basé sur la programmation fonctionnelle, et du cadre logique de vérification, basé sur la logique d'ordre supérieur.
Tous ces aspects reposent sur l'utilisation avancée de la notion de typage et sur les relations intimes entre types, spécifications, et calculs.

L'auteur Yves Bertot est chercheur à l'INRIA et travaille avec le système depuis une vingtaine d'années.  Il a utilisé ce système pour des études d'algorithmes en technologie des langages de programmation, géométrie, arithmétique des ordinateurs, ...

Ce cours vidéo s'adresse à un public informaticien avec des prérequis qui sont partagés par la majeure partie des ingénieurs du milieu industriel.

Les pictogrammes comme celui-ci indiquent une vidéo de démonstration d'utilisation de Coq, qui complémente le cours principal.

Les vidéos du cours


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  


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





Last modified: Wed Jul 19 10:06:16 CEST 2017