Preuves formelles en Coq

par Loïc Pottier

Niveau : Master   Langue : Français

Description :

Cours d'option en DEA de mathématiques, université de Nice-Sophia Antipolis, janvier 2003. Ce cours est inspiré du cours de DEA de Gilles Dowek, et du cours de DEA de Christine Paulin-Mohring et Benjamin Werner (DEA de programmation SPL, Paris).

Télécharger :

PDF (690.34ko)
PS (158.35ko)

Detail du cours

Tables des matières

Le langage de Coq
Les objets et la syntaxe
Les types
Les sortes
Les fonctions
Les formules logiques, leurs preuves, et l'isomorphisme de Curry-Howard
Le typage
Règles de typage informelles
Les règles du typage
Les contextes
Les jugements de typage
Les règles
Exemples
Quelques remarques sur les règles de typage des produits
Le calcul
La beta-réduction
La consistance
Logique intuitionniste et mathématiques constructives
Les définitions et la delta-réduction
La conversion
Exemple : les codages imprédicatifs
Les types inductifs
Exemples
Les entiers naturels
L'égalité de Leibniz
Raisonnement et calcul par cas : la construction Cases
La iota-réduction
Fonctions récursives : la construction Fix
Un exemple
Un exemple de récursion mutuelle
Le cas général
La iota-réduction, bis
Typage de Cases et Fix
Introduction au système Coq
Commandes élémentaires
Lancer coq depuis un shell
Obtenir le type d'un terme
Définir une constante
Obtenir la valeur d'une constante
Calculer
Fonctions récursives
Démontrer
pour tout A, A implique A
pour tout A, A implique non non A
Calcul des propositions
Calcul des prédicats
Exemples mathématiques
L'ensemble des parties est plus gros que l'ensemble

Source : http://www.librecours.org/cgi-bin/course?callback=info&am...

Modérateurs

Dimitri Ara, Romain Théret
Contact : logique AT librecours.org

Source : http://www.librecours.org/cgi-bin/domain?callback=info&am...