MCAL – Lambda-Calcul

resp. Pascal Fradet

UGA – L3 INFO – 2024-2025

On trouvera ici le support du cours de Lambda-calcul faisant partie avec le cours Machines de Turing du module Modèles de calcul (MCAL) des L3 Info de l’UGA. Le support comprend les transparents du cours, les fiches de TD, les fichiers Coq utiles pour les TDs et les annales de l’année passée.

• Cours

  • Le lambda-calcul pur                                                    (Résumé et exercices)

  • Codages et programmation en lambda-calcul pur

  • Le lambda-calcul typé

  • Extensions au lambda-calcul typé

• TDs

  • Fiche 1 (TD 1 & 2) : Syntaxe, portée et réduction

  • Fiche 2 (TD 3, 4 & 5) : Codages (booléens, entiers, paires, récursion)

  • Fiche 3  (TD 6, 7 & 8) : Lambda-calculs typés

• Fichiers Coq

Le fichier untypedLC.v contient l’interprète de lambda-calcul pur en Coq et différentes fonctions utiles pour les TD. Placez le dans votre répertoire de TD et compilez le dans coqide. Vous devriez voir apparaitre un fichier untypedLC.vo qui est utilisé par les fichiers Coq.

• • untypedLC.v

Les fichiers fichex.v contiennent un patron de script Coq utilisé par les fiches de TDs. Placez le dans votre répertoire de TD et complétez le suivant les instructions de la fiche de TD correspondante.

• • fiche1.v

  • fiche2.v

  • fiche3.v

• Annales

Les Quick et DS de MCAL-LC sont des QCM d’une heure corrigés par machine. Les questions évaluent votre compréhension et maîtrise des notions vues en cours et travaillées en TD. Les QCM  comportent également quelques questions de cours non revues en TD. Ceux de l’année passée sont accessibles ci-dessous

• • Quick du 22/02/2024

  • DS du 12/04/2024