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
7th March ~ 6th June, 2024
Location
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| Thursday | 08:30 - 11:45 | A3-3-201 | ZOOM 07 | 559 700 6085 | BIMSA |
Prerequisite
Discrete mathematics, mathematical logic
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.
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.
Audience
Graduate
Video Public
No
Notes Public
No
Language
Chinese
Lecturer Intro
Hanru Jiang is an Associate Researcher at BIMSA. He received his Ph.D. in Computer Science and Technology from the University of Science and Technology of China in 2019. From 2019 to 2020, he was an Assistant Researcher at the Quantum Computing Research Center, Peng Cheng Laboratory. His research interests lie in programming language theory, formal verification of compilers, and programming language issues in quantum computing. His work has been published in premier venues such as PLDI, CAV, and OOPSLA. He was a recipient of the PLDI 2019 Distinguished Paper Award.