程序设计语言的形式语义（Formal Semantics of Programming Languages）

学期：2020-2021学年第一学期

时间：周四1-2节，8:00am - 9:50am

地点：仙II-310

QQ群：917572937（进群请实名）

授课老师：梁红瑾，计算机系楼404室

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

期末考试时间：2020年12月31日周四1-2节，8:00am - 9:50am，地点：仙II-310，闭卷

Lecture Notes

• [09/10]: Introduction (notes), and Coq tutorial (Overview, and the Coq files used for the demo, which can be compiled with Coq 8.12.0). How to install Coq.
• [09/17]: Mathematical background (notes).
• [09/24]: Lambda calculus (notes). Read the first three sections of Peter Selinger's lecture notes. Also see Alligator Eggs for Untyped Lambda Calculus for fun.
• [10/10]: Lambda calculus (continued).
• [10/15]: Lambda calculus (continued), and simply-typed lambda calculus (notes). Read the type-safety proofs of Dan Grossman's lecture notes.
• [10/22]: Simply-typed lambda calculus (continued), and operational semantics (notes).
• [10/29]: Operational semantics (continued).
• [11/05]: Operational semantics (continued).
• [11/12]: Hoare logic (notes)
• [11/19]: Hoare logic (continued)
• [11/26]: Hoare logic (continued)
• [12/03]: Separation logic (notes). Read the notes by Reynolds.
• [12/10]: Separation logic (continued).
• [12/17]: Separation logic (continued).
• [12/24]: Shared-variable concurrency (notes). Review (notes).

Assignments

• [09/17] Assignment on mathematical background. Due by 23:59pm, 09/24.
• [10/15] Assignment on lambda calculus and types. Due by 23:59pm, 10/22.
• [11/05] Assignment on operational semantics. Due by 23:59pm, 11/12.
• [11/26] Assignment on Hoare logic. Due by 23:59pm, 12/03.

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)

最后更新日期：2020-12-23