Le cours était 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,
et les archives sont supprimées au bout d’un moment.
- Introduction
- Un avant-goût sur syntaxe/sémantique, avec les expressions polynomiales
- diapo
- Mise à niveau : propositions et prédicats
- Calcul propositionnel et calcul des prédicats : valeurs de vérités, équivalences, interprétations
- diapo
- exercices
- Mise à niveau : déduction
- Cours sur la déduction naturelle propositionnelle
- diapo
- vidéo
- exercices
- Mise à niveau : (in)complétude
- 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
- Une courte digression sur la quantification au second ordre
- diapo
- vidéo
- Calcul des séquents
- Cours sur les calculs des séquents intuitionniste et classique
- diapo
- vidéo
- Devoir à la maison : non-non-traduction
- sujet
- Élimination des coupures
-
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
- 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
- fiche d’activité
- λ-calcul simplement typé
- 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
- Devoir à la maison : réduction gauche
- sujet
- Au-delà des types simples
- 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