layout title permalink page Schedule /schedule/ Module Topics Reading 1 Introduction, Coq Basics, Functional Programming, Induction & Inductive Data Structures Intro Slides (PDF) Lec 2 Zoom Recording Lec2 Reading Lec3 Zoom Recording Lec3 Reading Lec4 Zoom Recording Lec4 Reading Lec5 Zoom Recording Lec5 Reading Lec6 Recording (from archive) 2 Polymorphism, Higher-Order Functions, Maps, Coq Tactics Lec7 Zoom Recording Lec8 Zoom Recording Lec7 & Lec8 Reading Lec 9 Recording (from archive) Lec 9 Reading Lec 10 Zoom Recording Lec 10 Reading </td> 3 Logic in Coq, Inductive Propositions, Curry-Howard Correspondence Course Project Proposals Lec 11 Zoom Recording Lec 11 Reading Lec 12 Zoom Recording Lec 12 Reading Lec 13 Zoom Recording Lec 13 Reading 4 Modeling an Imperative Language (Imp), Operational Semantics Lec 14 Zoom Recoding Lec 15 Zoom Recording Lec 16 Zoom Recording Lec 14-16 Reading 5 Reasoning about Imp using Hoare Logic Lec 17 Zoom Recording Lec 18 Zoom Recording Lec 19 Zoom Recording Lec 17-19 Reading Lec 20 Zoom Recording Lec 20-21 Reading Lec 21 Zoom Recording Lec 21 Reading 6 Small-Step Semantics Lec 22 Zoom Recording Lec 23 Zoom Recording Lec 22-23 Reading 7 Type Systems, Simply Typed & Untyped Lambda Calculus Lec 24 Zoom Recording Lec 24 Reading Lec 25 Zoom Recording part 1 Lec 25 Zoom Recording part 2 Lec 25 Class Notes