Cette année le cours est animé sur Ametice.
Je reproduis sur cette page les supports utilisés, parce qu’Amétice ne permet pas de publier le contenu des cours :
- Introduction (13 septembre)
- Un avant-goût sur syntaxe/sémantique, avec les expressions polynomiales
- diapo
- Mise à niveau : propositions et prédicats (13 septembre)
- Calcul propositionnel et calcul des prédicats : valeurs de vérités, équivalences, interprétations
- diapo
- exercices
- Mise à niveau : déduction (20 septembre)
- Cours sur la déduction naturelle propositionnelle
- diapo
- vidéo
- exercices
- Mise à niveau : (in)complétude (20 septembre)
- Cours sur la déduction naturelle au premier ordre, et les théorèmes de complétude et incomplétude de Gödel
- diapo
- vidéo
- exercices
- Logiques du second ordre (27 septembre)
- Une courte digression sur la quantification au second ordre
- diapo
- vidéo
- Calcul des séquents (4 octobre)
- Cours sur les calculs des séquents intuitionniste et classique
- diapo
- vidéo
- Devoir à la maison : non-non-traduction
- À rendre avant le 21 octobre (inclus).
- sujet
- Élimination des coupures (11 octobre)
-
Cours sur l’élimination des coupures en calcul des séquents : règles
d’élimination, preuve du théorème, conséquences sur la constructivité
de LJ, adaptation au cas de la déduction naturelle.
- diapo
- vidéo
- exercices
- λ-calcul (18 octobre)
- Introduction au λ-calcul et propriétés essentielles de la β-réduction : confluence et stratégie de normalisation
- diapo
- vidéo
- exercices
- Fiche d’activité : Calculabilité en λ-calcul
- À préparer pour le 3 novembre
- fiche d’activité
- λ-calcul simplement typé (8 novembre)
- Typage à la Church et à la Curry, correspondance de Curry-Howard et applications
- diapo
- vidéo
- exercices
- Fiche d’activité : Normalisation forte pour le λ-calcul simplement typé
-
Cette série d’exercices vous donne une preuve de la normalisation
forte en λ-calcul simplement typé. Il s’agit d’une preuve purement
arithmétique, qui ne peut pas se généraliser à des systèmes de types
plus riches. Mais elle permet de découvrir des propriétés importantes
sur la forte normalisabilité (celle de l’exercice 1 surtout). La
récurrence de l’exercice 2 est « amusante ».
- fiche pour démontrer la normalisation forte des termes simplement typés
- À préparer pour le 8 novembre (facultatif)
- Devoir à la maison : réduction gauche
- sujet
- À rendre avant les examens.
- Au-delà des types simples (15 novembre)
- Cours sur des extensions possibles du λ-calcul simplement typé :
- côté programmation : récursion, points fixes ;
- côté logique : types produits et sommes pour la déduction naturelle intuitionniste ;
- le second ordre : système F ;
- caractérisation de la normalisation : types avec intersection.
- diapo
- vidéo
- exercices
- Examen de l’année dernière
- sujet
- Examen final
- sujet