Séance de cours
Cette séance de cours couvre les règles de type en sémantique opérationnelle, assurant la vérification de type de programme, la solidité par le progrès et la préservation, et la preuve du progrès et de la préservation en utilisant l'induction sur les termes. Il traite également des fonctions définies par l'utilisateur et de la substitution dans les dérivations de type.