程序设计语言的形式语义

Speaker：Hanru Jiang

Date：Tues. & Thurs. 08:00-09:35，2021-02-22~05-16

Venue：BIMSA 1120 Room & Zoom ID：388 528 9728 Password：BIMSA

Abstract：

形式语义是进行程序语言研究的基础。本课程将介绍程序设计语言的形式语义，涵盖的内容包括λ演算、命令式语言的操作语义和Hoare逻辑、分离逻辑、并发语言、量子程序语言等。本课程还将介绍如何在Coq定理证明工具中形式化程序语言的语义并作推理。课程中的大部分结论将在Coq中给出机器可检查的证明。

Prerequisite：

基本的演绎推理知识和编程经验

References：

《Software Foundations》 Benjamin C. Pierce
《Theories of Programming Languages》 John C. Reynolds
《Practical Foundations for Programming Languages》Robert Harper