MATH0980 : contenu algorithmique des démonstrations mathématiques
Ce wiki est un complément pour le cours du Master deuxième année intitulé "contenu algorithmique des démonstrations mathématiques". Le cours est donné par Karim Nour et Pierre Hyvernat à l'université Claude Bernard, à Lyon...
Nous encourageons tous les étudiants à y participer en l'augmentant au fur et à mesure de l'avancement du cours.
Pour pouvoir modifier les pages, inscrivez-vous pour obtenir un login et mot de passe. (S'il vous plaît, utilisez votre vrai nom...)
Allez regarder ici pour vous familiariser avec les wikis.
Vous pouvez également utiliser la page de discussion pour ... discuter (ou poser des questions).
Exercice :
créez-vous un compte et essayez de modifier cette page (correction de fôtes d'aurtograffe, rajout de détails, mise en page, ...)
Details techniques / administratifs
Nouvelles
Les nouvelles importantes pour le cours (les plus récentes en haut).
Rq : pour mettre la date dans le wiki, il suffit de mettre "~~~~".
- Hyvernat 23 janvier 2008 à 09:23 (CET) : le cours a disparu, mais il revient ! Nous commencerons donc avec une semaine de retard...
- Hyvernat 4 janvier 2008 à 14:16 (CET) : création du wiki.
Plan (provisoire) du cours
Comme nous commençons avec une semaine de retard, il faudra ajuster ce plan : soit en décalant les seances, soit en rattrapant les deux heures du 17 janvier en rallongeant d'autres séances...
- Séance 1 : 17 janvier (KN) Présentation du cours ; déduction naturelle et traduction de Gödel.
- Séance 2 : 24 janvier (KN) Sémantiques pour les logiques classiques et intuitionniste.
- Séance 3 : 31 janvier (KN) Calcul des séquents et élimination des coupures.
- Séance 4 : 7 février (PH) Introduction au lambda-calcul : Church-Rosser.
- Séance 5 : 14 février (PH) Représentation des fonctions récursives.
- Séance 6 : 28 février (PH) Lambda-calcul typé : préservation de type et forte normalisation.
- Séance 7 : 6 mars (PH) Fonctions représentables en lambda-calcul typé.
- Séance 8 : 13 mars (KN et/ou PH) Contrôle.
- Séance 9 : 20 mars (KN) Lambda-mu-calcul : Church-Rosser et préservation de type.
- Séance 10 : 27 mars (KN) Plusieurs preuves de forte normalisation du lambda-mu-calcul typé.
- Séance 11 : 3 avril (KN) Entiers classiques et mise en mémoire.
- Séance 12 : 10 avril (PH) Sémantique du lambda-calcul (1).
- Séance 13 : 17 avril (PH) Sémantique du lambda-calcul (2).
- Séance 14 : 24 avril (KN et/ ou PH) Examen final.
Contenu des séances
Séance 1
-- à compléter au fur et à mesure --
Quelques références
- logique générale : "Introduction à la Logique Théorie de la démonstration" de René David, Karim Nour et Christophe Raffalli ; édité par Dunod. (Voir ici pour plus de détails...)
- lambda-calcul : "Lambda-calcul, types et modèles" de Jean-Louis Krivine ; édité par Masson (1990). Cet ouvrage est epuisé, mais il y en a deux exemplaires à la bibliothèque de mathématiques. JL Krivine a également mis la version anglaise de son livre sur sa page web
- pour un éclairage très différent du même sujet, vous pouvez lire les notes de Thierry Coquand.
Contenu algorithmique des démonstrations mathématiques
Introduction
-- à compléter --
Déduction naturelle et traduction de Gödel
blabla
...