摘  要：

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

预备知识：

基本的编程经验

参考书目：

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。