Logical Formulas and Types: Understanding the Kerry Howard Isomorphism

This lecture focuses on understanding the Kerry Howard Isomorphism, which relates logical propositions to types and proofs to terms. The instructor guides the students through exercises where they write terms corresponding to logical formulas using this isomorphism. The lecture covers topics such as pairs, functions, and sums in the context of constructive logic and simply typed lambda calculus. The instructor explains the process of translating propositions into types and terms, emphasizing the importance of following the types to write correct terms. The lecture also includes a detailed walkthrough of a proof by induction on subtyping rules, demonstrating how to apply the rules to derive conclusions. The instructor provides insights into exam preparation, highlighting the need to review course materials and practice exercises to be well-prepared for the exam.