助教：范伟杰，计算机系楼409室

期末考试时间：2021年12月23日周四1-2节，8:00am - 9:50am，地点：逸B-205，闭卷

Lecture Notes

• [09/02]: Introduction (notes), and Coq tutorial (Overview, and the Coq files used for the demo, which can be compiled with Coq 8.13.2). How to install Coq.
• [09/09]: Mathematical background (notes).
• [09/16]: Lambda calculus (notes). Read the first three sections of Peter Selinger's lecture notes. Also see Alligator Eggs for Untyped Lambda Calculus for fun.
• [09/23]: Lambda calculus (continued).
• [09/30]: Lambda calculus (continued), and simply-typed lambda calculus (notes). Read the type-safety proofs of Dan Grossman's lecture notes.
• [10/09]: Simply-typed lambda calculus (continued).
• [10/14]: Operational semantics (notes).
• [10/21]: Operational semantics (continued).
• [10/28]: Operational semantics (continued), and Hoare logic (notes).
• [11/04]: Hoare logic (continued).
• [11/11]: Hoare logic (continued).
• [11/18]: Hoare logic (continued).
• [11/25]: Separation logic (notes). Read the notes by Reynolds.
• [12/02]: Separation logic (continued).
• [12/09]: Separation logic (continued).
• [12/16]: Shared-variable concurrency (notes), and review (notes).

Assignments

• [09/09] Assignment on mathematical background. Due by 23:59pm, 09/16.
• [10/09] Assignment on lambda calculus and types. Due by 23:59pm, 10/21.
• [10/28] Assignment on operational semantics. Due by 23:59pm, 11/04.
• [11/18] Assignment on Hoare logic. Due by 23:59pm, 11/25.

Textbooks and References

• Textbooks: lecture notes and handouts
• References:
• Benjamin C. Pierce, et al. Software Foundations
• John C. Reynolds. Theories of Programming Languages, Cambridge University Press.
• Hanne Riis Nielson, Flemming Nielson. Semantics with Applications: A Formal Introduction.
• Robert Harper. Practical Foundations for Programming Languages. (The online abridged preview edition)

最后更新日期：2021-12-15