MCAL – Lambda-Calcul

resp. Pascal Fradet

UGA – L3 INFO – 2023-2024

On trouvera ici les supports 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, deux fichiers Coq utiles pour les TDs et quelques annales.

• 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 devrez voir apparaitre un fichier untypedLC.vo qui est importable dans vos fichiers Coq.

• untypedLC.v

Le fichier extLC.v contient un patron de script Coq utilisé par la dernière partie de la fiche 3 des TDs. Placez le dans votre répertoire de TD et complétez le suivant les instructions du TD.

• extLC.v

• Annales

• • DS du 01/03/2023

  • DS du 04/04/2023

  • DS du 20/02/2024