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

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

Lecture Notes

• [09/04]: Introduction (notes), and Coq tutorial (Overview, and the Coq file used for the demo, which can be compiled with Coq 8.18.0 in release 2023.11.0). How to install Coq.
• [09/11]: Mathematical background (notes).
• [09/18]: 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/25]: Lambda calculus (continued).
• [10/09]: Lambda calculus (continued), and simply-typed lambda calculus (notes). Read the type-safety proofs of Dan Grossman's lecture notes.
• [10/16]: Simply-typed lambda calculus (continued).
• [10/23]: System F (notes).
• [10/30]: System F (continued), and operational semantics of imperative languages (notes).
• [11/06]: Operational semantics (continued).
• [11/13]: Operational semantics (continued).
• [11/20]: Operational semantics (continued), and Hoare logic (notes).
• [11/27]: Hoare logic (continued).
• [12/04]: Hoare logic (continued).
• [12/11]: Hoare logic (continued). Separation logic (notes). Read the notes by Reynolds.
• [12/18]: Separation logic (continued). Review (notes).

Assignments

• [10/09]: Assignment on lambda calculus and types. Due by 23:59pm, 10/16.
• [11/13]: Assignment on operational semantics. Due by 23:59pm, 11/20.
• [12/04]: Assignment on Hoare logic. Due by 23:59pm, 12/11.

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.
• Benjamin C. Pierce. Types and Programming Languages. The MIT Press.

最后更新日期：2024-12-17