Logique et automates

M2 IMD, 2022—2023 (archive)

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

Dernière mise à jour
le 28 janvier 2025.

XHTML et CSS valides?