摘 要:
形式语义是进行程序语言研究的基础。本课程将介绍程序设计语言的形式语义,涵盖的内容包括λ演算、命令式语言的操作语义和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。