Types dans Lambda Calculus

Cette séance de cours introduit le concept de types dans le calcul lambda, en se concentrant sur deux langages dexemples: taper des expressions arithmétiques et simplement taper le calcul lambda. L'instructeur explique comment définir des types, spécifier des règles de frappe et prouver la solidité. La séance de cours couvre des sujets tels que les règles d'évaluation, la sécurité de type, l'algorithme de vérification de type, les formes canoniques, la progression, la préservation et les propriétés de la relation de frappe.