Simply Taped Lambda Calculus: Fondements et propriétés

Cette séance de cours présente le calcul lambda (STLC) simplement typé, en se concentrant sur sa syntaxe, sa sémantique et son système de type. L'instructeur commence par discuter des concepts fondamentaux du calcul lambda, y compris l'abstraction fonctionnelle, la substitution et la réduction. La séance de cours met l'accent sur l'importance des systèmes de type dans les langages de programmation, soulignant les propriétés attendues d'eux, telles que le progrès et la préservation. L'instructeur définit la syntaxe de STLC, en incorporant des variables, des constantes et des applications de fonctions. La sémantique est alors établie, détaillant comment les expressions peuvent être évaluées et réduites. La séance de cours couvre également les définitions inductives des règles de dactylographie, démontrant comment déterminer si les expressions sont bien typées. L'instructeur illustre l'importance de ces règles à travers des exemples, mettant en évidence les défis posés par les variables liées et les substitutions. Enfin, la séance de cours se termine par une discussion sur la solidité du système de type, prouvant que les programmes bien typés évaluent les valeurs ou peuvent progresser, en veillant à ce qu'ils ne deviennent pas bloqués dans des états non terminaux.