Brief Introduction to the Rocq (Coq) Prover
In this course we briefly introduce the Rocq theorem prover, in the context of programming language research. By the end of this course, we will build a verified checker for a simple program logic.
Lecturer
Date
20th April ~ 29th June, 2026
Location
| Weekday | Time | Venue | Online | ID | Password |
|---|---|---|---|---|---|
| Monday | 20:10 - 21:45 | A14-102 | Tencent A | 482 969 7386 | 106457 |
Audience
Graduate
Video Public
Yes
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.