Master Parisien de Recherche en Informatique
2009-10
cours 2-7-2
Assistants de preuve
Christine Paulin-Mohring, Benjamin Werner,
Bruno Barras, Hugo Herbelin,
Jean-Christophe Filliâtre, Claude Marché
Introduction au Calcul des Constructions Inductives
Motivations
Quelques rappels sur les théories de types
Un premier contact avec Coq: Curry-Howard en action
Les Entiers Naturels dans CCI
D’autres types de données courants
Types inductifs plus complexes
Prédicats inductifs
Exemple de développement Gallina : Sémantique d’un mini-langage
Introduction
Présentation du problème
Spécification
Gallina
Pour en savoir plus
Types inductifs
Généralités
Les déclarations non-récursives
Les types inductifs récursifs
Extensions
Types coinductifs dans Coq
Introduction
Exemple des listes infinies
Définition des types co-inductifs dans Coq
Applications
Architecture des assistants à la démonstration
Architecture de Coq
Critères de classification
Autres systèmes
Preuves par réflexion
Extraction de programmes et réalisabilité
Introduction
Interprétation constructive des preuves
Réalisabilité
Réalisabilité dans le Calcul des Constructions
L’extraction en pratique
Preuve de programmes fonctionnels
Méthode directe
Utilisation de types dépendants
Modules et foncteurs
Preuve de programmes impératifs
Logique de Hoare classique
Transformation fonctionnelle : la méthode Why
Traitement des structures données complexes et application à d’autres langages de programmation
Sémantique du Calcul des Constructions Inductives
Le Calcul des Constructions pur (CC)
Le Calcul des Constructions avec univers (CC
ω
)
Extensions cohérentes et incohérentes du Calcul des Constructions Inductives
Références
Ce document a été traduit de L
A
T
E
X par
H
E
V
E
A