Formal Semantics of Programming Languages
In this course, we study methods to define the behaviors of programs and approaches to reason about the properties of programs. We will introduce lambda calculus, operational semantics, denotational semantics, Hoare logic, separation logic, concurrent separation logic, etc. We also practice building verified programs using Coq.
Lecturer
Date
14th March ~ 6th June, 2023
Location
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| Tuesday | 13:30 - 16:55 | A3-2-301 | ZOOM 06 | 537 192 5549 | BIMSA |
Prerequisite
Discrete mathematics, algorithms, and elementary logic
Syllabus
Lambda calculus
Simply-typed lambda calculus
Operational semantics
Denotational semantics
Hoare logic
Separation logic (SL)
Concurrency and CSL
Semantics of probabilistic programming
Semantics of quantum programs
Simply-typed lambda calculus
Operational semantics
Denotational semantics
Hoare logic
Separation logic (SL)
Concurrency and CSL
Semantics of probabilistic programming
Semantics of quantum programs
Reference
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.
Audience
Graduate
Video Public
No
Notes Public
No
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.