程序设计语言的形式语义
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