Designing Calculi: Strong Normalization and Error Handling

This lecture focuses on the theoretical side of designing Calculi, specifically on strong normalization of linear SDLC and error handling. The instructor guides the audience through proving lemmas, understanding calculus adjustments, and applying induction on term structures. The session covers the importance of intuition before diving into proofs, the application of typing rules, and the evaluation of reduction rules. The audience is encouraged to think about how to type functions that may or may not perform errors, and to write typing rules ensuring progress and preservation. The lecture concludes with a dry run for an upcoming online exam, where participants are asked to solve exercises on paper and submit them for verification.