学期：2026-2027学年第一学期
上课时间地点：周三3-4节，10:10 - 12:00，仙I-216
Office Hours：周三下午15:00-17:00，计算机楼404室
授课老师：梁红瑾，计算机楼404室
助教：待定
期中考试时间地点：2026年10月28日课堂上，闭卷
| Dates | Lectures | Reading Materials | Homework | Solutions |
|---|---|---|---|---|
| 08/26 | Introduction (notes), and Rocq tutorial (Overview, and the Rocq file used for the demo, which can be compiled with Rocq 9.2.0). | You could install Rocq following the instructions on the official website. | — | — |
| 09/02 | Mathematical background (notes). | — | — | — |
| 09/09 | Lambda calculus (notes). | See Alligator Eggs for Untyped Lambda Calculus for fun. | HW1-lambda.pdf, due by next class (09/16, 10:10 am). | HW1 |
| 09/16 | Lambda calculus (continued). | Read the first three sections of Peter Selinger's lecture notes. | HW2-lambda.pdf, due by next class (09/23, 10:10 am). | HW2 |
| 09/23 | Simply-typed lambda calculus (notes). | Read the type-safety proofs of Dan Grossman's lecture notes. | HW3-types.pdf, due by next class (09/30, 10:10 am). | HW3 |
| 09/30 | Simply-typed lambda calculus (continued). | — | HW4-types.pdf, due by next class (10/10, 10:10 am). | HW4 |
| 10/10 | System F (notes). | — | HW5-systemF-erasure.pdf, due by next class (10/14, 10:10 am). | HW5 |
| 10/14 | System F-omega (notes). | — | — | — |
| 10/21 | Mid-term review (notes). Operational semantics of imperative languages (notes). | — | — | — |
| 10/28 | Mid-term exam. | — | — | — |
最后更新日期：2026-10-20