Ok

En poursuivant votre navigation sur ce site, vous acceptez l'utilisation de cookies. Ces derniers assurent le bon fonctionnement de nos services. En savoir plus.

03/01/2010

Preuves formelles en Coq

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)
Licence Libre Cours Type 4

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 AraRomain Théret
Contact : logique AT librecours.org

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

10:51 Publié dans Preuves formelles en Coq | Lien permanent | Commentaires (0) | Tags : preuves formelles en coq | |  del.icio.us | | Digg! Digg |  Facebook

Les commentaires sont fermés.