程序语言的形式语义
形式语义是进行程序语言研究的基础。本课程将介绍程序设计语言的形式语义，涵盖的内容包括λ演算、命令式语言的操作语义和Hoare逻辑、分离逻辑等。本课程还将介绍如何在Coq定理证明工具中形式化程序语言的语义并作推理。
讲师
日期
2022年03月17日 至 06月09日
网站
修课要求
基本的编程经验
参考资料
1. Benjamin C. Pierce, et al. Software Foundations. 2. John C. Reynolds. Theories of Programming Languages.
视频公开
不公开
笔记公开
不公开
讲师介绍
蒋瀚如于2019年在中国科学技术大学取得计算机科学与技术博士学位，2019-2020年在鹏城实验室量子计算研究中心担任助理研究员，2020年加入BIMSA任助理研究员。他的主要研究方向为程序语言理论、编译器的形式化验证和量子计算中的程序语言问题。作为并发程序分离编译验证工作CASCompCert的主要完成人，获得程序语言领域顶级会议PLDI 2019的Distinguished Paper Award。