学期：2026-2027学年第一学期
上课时间地点：周三3-4节，10:10 - 12:00，仙I-216
Office Hours：周三下午15:00-17:00，计算机楼404室
授课老师：梁红瑾，计算机楼404室
助教：待定
| 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). | — |
| 09/30 | Simply-typed lambda calculus (continued), and system F (notes). | — | HW4-types.pdf, due by next class (10/10, 10:10 am). | — |
最后更新日期：2026-09-29