助教：林荣恩，计算机系楼409室

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

Lecture Notes

• [09/06]: Introduction (notes), and Coq tutorial (Overview, and the Coq files used for the demo, which can be compiled with Coq 8.16.1 with 2022.09 release). How to install Coq.
• [09/13]: Mathematical background (notes).
• [09/20]: 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/27]: Lambda calculus (continued).
• [10/11]: Lambda calculus (continued), and simply-typed lambda calculus (notes). Read the type-safety proofs of Dan Grossman's lecture notes.
• [10/18]: Simply-typed lambda calculus (continued), and operational semantics (notes).
• [10/25]: Operational semantics (continued).
• [11/01]: Operational semantics (continued).
• [11/08]: Operational semantics (continued), and Hoare logic (notes).
• [11/15]: Hoare logic (continued).
• [11/22]: Hoare logic (continued).
• [11/29]: Hoare logic (continued).
• [12/06]: Separation logic (notes). Read the notes by Reynolds.
• [12/13]: Separation logic (continued).
• [12/20]: Separation logic (continued). Review (notes).

Assignments

• [10/11]: Assignment on lambda calculus and types. Due by 23:59pm, 10/18.
• [11/08]: Assignment on operational semantics. Due by 23:59pm, 11/15.
• [11/29]: Assignment on Hoare logic. Due by 23:59pm, 12/06.

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)
• Glynn Winskel. The Formal Semantics of Programming Languages: An Introduction. The MIT Press.

最后更新日期：2023-12-19