Cheng Zhang
I am an incoming postdoc research fellow at UCL Programming Principles, Logic, and Verification Group, working with Professor Alexandra Silva. Prior to that, I was a Ph.D. student at Boston University supervised by Professor Marco Gaboardi.
My works range over a wide spectrum of theoretical and real-world problems in the field of Kleene Algebra.
- On the theoretical side, I am interested in producing simple and elegant proofs of complicated results like completeness and decidablity. Many of my theoretical work is built upon beautiful ideas from universal algebra, coalgebra, and category theory.
- On the practical side, I am interested in all kinds of applications of Kleene Algebra in various field of computer science, including network, distributed system, probabilistic computing, etc. Currently, most of my practical work is in the field program logics and verifications. However, I am eager to use the power of Kleene Algebra to tackle real-world problems in other fields of Computer Science.
You can find out more about my research and experiences in my CV and research statement
News
Oct 2024 --- Our paper "CF-GKAT: Efficient Validation of Control-Flow Transformations" is conditionally accepted at POPL 2025. Hope to see you at Denver, Colorado!
Sep 2024 --- I will be attending NEPLS 2024 at NEU!
Sep 2024 --- I am joining PPLV groups of UCL as a postdoc!
Aug 2024 --- I have finished my Ph.D. at Boston University!
Publications and Preprints
-
Efficient Symbolic Algorithms For GKAT equivalence
[implementation] (Draft) -
CF-GKAT: Efficient Validation of Control-Flow
Transformations
(Conditionally Accepted at POPL 2025) -
Kleene algebra with commutativity conditions is undecidable
[hal] (Under Submission) -
Domain Reasoning In TopKAT
[arxiv] [doi] (ICALP2024) -
A Dependently Typed Language with Dynamic Equality
[doi] (TyDe2023) -
On Incorrectness Logic and Kleene Algebra With Top and Tests
[arxiv] [doi (contains errors)] (POPL2022) -
Developing a Dependently Typed Language with Runtime Proof Search (Extended
Abstract)
[ICFP website] (TyDe2020) -
Kings in Generalized Tournaments
[archive] (Honor Thesis) -
Lexos 2017: Building Reliable Software in Python
[doi] (CCSC2018)
Hobbies
I enjoy cooking, food, coffee, gardening with my wife, and hang out with my pet rabbits. I sometimes read about coffee and old Chinese poetry; I kept a tiny blog of some poetries and lyrics I translated and wrote. These translations are generally terrible, but I am trying to get better.
Teaching
- 2020 Fall, CS 230: Principle of Programming Language, with Professor Marco Gaboardi and Lecture Abbas Attarwala
- 2020 Summer, CS 111: Introduction to Computer Science 1, with Lecture John Magee
- 2020 Summer, CS 112: Introduction to Computer Science 2, with Lecturer Christine Papadakis-Kanaris
- 2020 Spring, CS 235: Algebraic Algorithm, with Professor Leonid Levin
- 2019 Fall, CS 132: Geometric Algorithm, with Lecture Abbas Attarwala
- 2019 Spring, CS 230: Principle of Programming Language, with Professor Wayne Snyder
Name Pronunciation
Quotes
- Throughout my whole life as a mathematician, the possibility of making explicit, elegant computations has always come out by itself, as a byproduct of a thorough conceptual understanding of what was going on. -- Alexander Grothendieck
- Simplicity is a great virtue but it requires hard work to achieve it and education to appreciate it. And to make matters worse: complexity sells better. -- Edsger W. Dijkstra
- Don't blame me for the fact that competent programming, as I view it as an intellectual possibility, will be too difficult for "the average programmer" — you must not fall into the trap of rejecting a surgical technique because it is beyond the capabilities of the barber in his shop around the corner. -- Edsger W. Dijkstra
- Either mathematics is too big for the human mind, or the human mind is more than a machine. -- Kurt Gödel
- It is impossible to be a mathematician without being a poet in soul. -- Sofia Kovalevskaya