程序语言的形式语义
本课程介绍如何严格地定义程序的行为、推理程序的性质。我们将介绍lambda-calculus、程序的操作语义和指称语义、Hoare逻辑、分离逻辑、并发分离逻辑等内容。我们还将在Coq定理证明工具中练习程序的形式验证。
讲师
日期
2023年03月14日 至 06月06日
位置
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| 周二 | 13:30 - 16:55 | A3-2-301 | ZOOM 06 | 537 192 5549 | BIMSA |
修课要求
Discrete mathematics, algorithms, and elementary logic
课程大纲
Lambda演算
简单类型的lambda演算
操作语义
指称语义
Hoare逻辑
分离逻辑
并发分离逻辑
概率程序语义
量子程序语义
简单类型的lambda演算
操作语义
指称语义
Hoare逻辑
分离逻辑
并发分离逻辑
概率程序语义
量子程序语义
参考资料
1. Robert Harper. Practical Foundations for Programming Languages.
2. John C. Reynolds. Theories of Programming Languages.
3. Viktor Vafeiadis. Concurrent separation logic and operational semantics
4. Fredrik Dahlqvist, Alexandra Silva and Dexter Kozen. Semantics of Probabilistic Programming: A Gentle Introduction
5. Mingsheng Ying. Foundations of Quantum Programming.
6. Benjamin C. Pierce, et al. Software Foundations.
2. John C. Reynolds. Theories of Programming Languages.
3. Viktor Vafeiadis. Concurrent separation logic and operational semantics
4. Fredrik Dahlqvist, Alexandra Silva and Dexter Kozen. Semantics of Probabilistic Programming: A Gentle Introduction
5. Mingsheng Ying. Foundations of Quantum Programming.
6. Benjamin C. Pierce, et al. Software Foundations.
听众
Graduate
视频公开
不公开
笔记公开
不公开
语言
中文
讲师介绍
蒋瀚如于2019年在中国科学技术大学取得计算机科学与技术博士学位，2019-2020年在鹏城实验室量子计算研究中心担任助理研究员，2020年加入BIMSA任助理研究员。他的主要研究方向为程序语言理论、编译器的形式化验证和量子计算中的程序语言问题。作为并发程序分离编译验证工作CASCompCert的主要完成人，获得程序语言领域顶级会议PLDI 2019的Distinguished Paper Award。