Cheng Zhang

Photo of me enjoying some Wendy's spicy chicken nuggets (not sponsored)

I am a 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 spectrum of practical and theoretical problems in the field of Kleene Algebra.

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

You can find out more about my research, teaching, and experiences in my research statement, teaching statement, DEI statement, and CV.

News

Nov 2024 --- Our paper "CF-GKAT: Efficient Validation of Control-Flow Transformations" is accepted at POPL 2025. Hope to see you in Denver, Colorado!

Oct 2024 --- Our paper "Kleene algebra with commutativity conditions is undecidable" is accepted at CSL 2025.

Oct 2024 --- I have joined PPLV groups of UCL as a postdoc! I am honored to work with Prof. Alexandra Silva, and her talented group.

Sep 2024 --- I will be attending NEPLS 2024 at NEU!

Aug 2024 --- I have finished my Ph.D. at Boston University!

Publications and Preprints

Efficient Symbolic Algorithms For GKAT equivalence
with Qiancheng Fu, Ji Hang, Ines Santacruz, Marco Gaboardi
[implementation] (Draft)
CF-GKAT: Efficient Validation of Control-Flow Transformations
with Tobias Kappé, David E. Narváez, Nico Naus
[arxiv] Principles of Programming Languages (POPL 2025)
Kleene Algebra with Commutativity Conditions is Undecidable
with Arthur Azevedo de Amorim, Marco Gaboardi
[arxiv] [hal] Computer Science Logic (CSL 2025)
Domain Reasoning In TopKAT: Reduction and Completeness
with Arthur Azevedo de Amorim, Marco Gaboardi
Theory and Practice of Static Analysis (TPSA 2025)
Two Variants of Kleeen Algebra and Their Applications
Cheng Zhang
Ph.D Thesis 2024
Domain Reasoning In TopKAT
with Arthur Azevedo de Amorim, Marco Gaboardi
[arxiv] [doi] International Colloquium on Automata, Languages, and Programming (ICALP 2024)
A Dependently Typed Language with Dynamic Equality
with Mark Lemay, Qiancheng Fu, William Blair, Hongwei Xi
[doi] Type-Driven Development (TyDe 2023)
On Incorrectness Logic and Kleene Algebra With Top and Tests
with Arthur Azevedo de Amorim, Marco Gaboardi
[arxiv] [doi (contains errors)] Principles of Programming Languages (POPL 2022)
Developing a Dependently Typed Language with Runtime Proof Search (Extended Abstract)
with Mark Lemay, William Blair
[ICFP website] Type-Driven Development (TyDe 2020)
Kings in Generalized Tournaments
Cheng Zhang
[archive] Undergraduate Honor Thesis 2018
Lexos 2017: Building Reliable Software in Python
with Weiqi Feng, Emma Steffens, Alvaro de Landaluce, Scott Kleinman, Mark D. LeBlanc
[doi] Journal of Computing Sciences in Colleges (CCSC 2018)

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

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.

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
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
@wilbowma I study computers so that I may one day defeat them -- Max S. New [link]