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

期末考试时间：2022年12月14日周三1-2节，8:00am - 9:50am，地点：仙II-103，闭卷

Lecture Notes

• [09/07]: Introduction (notes), and Coq tutorial (Overview, and the Coq files used for the demo, which can be compiled with Coq 8.15.2). How to install Coq.
• [09/14]: Mathematical background (notes).
• [09/21]: 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/28]: Lambda calculus (continued).
• [10/05]: Lambda calculus (continued), and simply-typed lambda calculus (notes). Read the type-safety proofs of Dan Grossman's lecture notes.
• [10/12]: Simply-typed lambda calculus (continued), and operational semantics (notes).
• [10/19]: Operational semantics (continued).
• [10/26]: Operational semantics (continued).
• [11/02]: Operational semantics (continued), and Hoare logic (notes).
• [11/09]: Hoare logic (continued).
• [11/16]: Hoare logic (continued).
• [11/23]: Hoare logic (continued).
• [11/30]: Separation logic (notes). Read the notes by Reynolds.
• [12/07]: Separation logic (continued). Review (notes).

Assignments

• [09/14]: Assignment on mathematical background. Due by 23:59pm, 09/21.
• [10/12]: Assignment on lambda calculus and types. Due by 23:59pm, 10/19.
• [11/02]: Assignment on operational semantics. Due by 23:59pm, 11/09.
• [11/23]: Assignment on Hoare logic. Due by 23:59pm, 11/30.

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)

最后更新日期：2022-12-06