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.
Lecturer
Date
20th March ~ 10th July, 2025
Location
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| Thursday | 09:50 - 12:15 | A3-2a-201 | ZOOM 01 | 928 682 9093 | BIMSA |
Syllabus
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
Reference
1. Benjamin C. Pierce, et al. Software Foundations.
2. John C. Reynolds. Theories of Programming Languages.
2. John C. Reynolds. Theories of Programming Languages.
Audience
Advanced Undergraduate
, Graduate
Video Public
No
Notes Public
Yes
Language
Chinese
Lecturer Intro
Hanru Jiang obtained a Ph.D. in computer science and technology from the University of Science and Technology of China in 2019. From 2019 to 2020, he worked as an assistant research fellow at the Quantum Computing Research Center of Pengcheng Laboratory. In 2020, he joined BIMSA as an assistant professor. His main research directions are programming language theory, compiler verification, and programming language aspects in quantum computing. As the main contributor to the concurrent program separation compilation verification work CASCompCert, won the Distinguished Paper Award of PLDI 2019, a top conference in the field of programming languages.