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 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.