Concevoir des calculs : forte normalisation et gestion des erreurs

Cette séance de cours se concentre sur le côté théorique de la conception Calculi, en particulier sur la normalisation forte de SDLC linéaire et la gestion des erreurs. L'instructeur guide le public en prouvant les lemmes, en comprenant les ajustements de calcul et en appliquant l'induction sur les structures de termes. La session couvre l'importance de l'intuition avant de plonger dans les preuves, l'application des règles de dactylographie et l'évaluation des règles de réduction. Le public est encouragé à réfléchir à la façon de taper des fonctions qui peuvent ou non effectuer des erreurs, et à écrire des règles de frappe assurant le progrès et la préservation. La séance de cours se termine par une course à sec pour un examen en ligne à venir, où les participants sont invités à résoudre des exercices sur papier et à les soumettre à la vérification.