Formal Semantics of Programming Languages
In this course we will study methods to define behaviors of programs, and methods to reason about properties of programs. We will practice formalizing semantics and building verified programs using Coq.
讲师
日期
2024年03月07日 至 06月06日
位置
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| 周四 | 08:30 - 11:45 | A3-3-201 | ZOOM 07 | 559 700 6085 | BIMSA |
修课要求
Discrete mathematics, mathematical logic
课程大纲
Lambda calculus
Simply-typed lambda calculus
Operational semantics
Denotational semantics
Hoare logic
Separation logic
Concurrency and Concurrent Separation Logic (CSL)
Categorical semantics of quantum programs
Simply-typed lambda calculus
Operational semantics
Denotational semantics
Hoare logic
Separation logic
Concurrency and Concurrent Separation Logic (CSL)
Categorical semantics of quantum programs
参考资料
1. 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. Chris Heunen and Jamie Vicary. Categories for Quantum Theory: An Introduction.
2. John C. Reynolds. Theories of Programming Languages.
3. Viktor Vafeiadis. Concurrent separation logic and operational semantics.
4. Chris Heunen and Jamie Vicary. Categories for Quantum Theory: An Introduction.
听众
Graduate
视频公开
不公开
笔记公开
不公开
语言
中文
讲师介绍
蒋瀚如，现任BIMSA副研究员。他于2019年在中国科学技术大学获得计算机科学与技术博士学位。2019年至2020年间，在鹏城实验室量子计算研究中心担任助理研究员。主要研究方向包括程序设计语言理论、编译器的形式化验证以及量子计算中的程序语言问题。其研究成果多次发表于 PLDI、CAV、OOPSLA 等程序语言领域的顶尖国际会议及期刊，曾获 PLDI 2019 杰出论文奖。