Inria
Inria.fr
Inria Channel
École CEA-EDF-Inria
Modélisation et vérification d'algorithmes en coq - une introduction
Cette école CEA-EDF-Inria abordera les techniques de base en modélisation et vérification d'algorithmes en Coq. Elle s'adresse aux étudiants, chercheurs ou ingénieurs qui ont une bonne connaissance de la programmation dans un langage conventionnel (C, Java).
- Date : 14/11/2011 au 18/11/2011
- Lieu : Inria - Antenne Parisienne, 23 avenue d'Italie - Paris 13ème
- Intervenants : Yves Bertot (Inria), Pierre Castéran (U Bordeaux), Benjamin Gregoire (Inria), Pierre Letouzey (U. Denis Diderot), Assia Mahboubi (Inria).
- Organisateurs : Francesco Zappa Nardelli
Objectifs :
Le système Coq fournit un langage de programmation fonctionnelle et un cadre de raisonnement basé sur la logique d'ordre supérieur pour effectuer des preuves sur les programmes. Le pouvoir expressif du langage est tel que l'on peut envisager des preuves sur des notions de mathématiques très avancées (comme le théorème des 4 couleurs) ou des programmes de complexité importante (comme un compilateur pour un noyau significatif du langage C). Dans ce cours, nous aborderons les techniques de base de la programmation dans ce langage et de la démonstration sur les programmes obtenus. Les concepts abordés seront : programmation récursive structurelle, manipulations de listes et d'entiers, démonstration par récurrence, définition récursive de types de données, constructions de filtrage et raisonnement par cas, propriétés inductives.
Programme :
| Les cours commenceront lundi 14 juin à 10h et se termineront vendredi 18 à 16h |
|
|---|---|
| Lundi |
Eléments de programmation fonctionnelle typée : programmation sans effets de bord, filtrage, fonctions anonymes, types prédéfinis simples nombres, booléens, listes, éléments de programmation d'ordre supérieure. Programmation récursive simple sur les nombres et les listes: introduction à la récursion structurelle |
| Mardi |
Construction et preuves de formules logiques : quantificateurs et connecteurs logiques, égalité, prédicats prédéfinis sur les nombres et les listes. Démonstration de formules simple en Coq: preuve dirigée par les buts |
| Mercredi |
Vérification de formules logiques simples concernant des programmes Preuves par récurrence sur les nombres et les listes. Nouveaux types de données et nouveau principes de raisonnement associés |
| Jeudi |
Prédicats inductifs et introduction aux types dépendants. Preuves par récurrence sur les prédicats inductifs. Notions de récursion géneralisée et de fonctions à type dépendant |
| Vendredi |
Études de cas |
Le nombre de participants étant limité, une pré-inscription est obligatoire. Lors de la pré-inscription vous êtes encouragés à expliquer brièvement pourquoi vous devriez et souhaitez assister à l'école
Les pré-inscriptions seront closes le 15 septembre. A l'issue de celle-ci toutes les demandes seront examinées afin d'obtenir une répartition équitable des 30 places parmi les candidats qualifiés. Les candidats de l'industrie sont fortement encouragés à postuler.
Tous les candidats recevront un avis le 20 septembre. Toute personne admise devra ensuite s'inscrire de façon définitive avant le 1er octobre 2011.
Frais d'inscription
- Membres Inria : gratuit
- Etudiants : 100 euros
- Académie : 300 euros
- Plein tarif : 600 euros
Ils comprennent la participation à l'école, les pauses-café et les repas du 14 au 18 novembre 2011.
Mots-clés : Méthodes formelles Assistant de preuve Coq Algorithmes
Partenaires
