Carview!

CARVIEW

MOTORHOMES

Select Language

HTTP/2 200 allow: GET, HEAD, OPTIONS alt-svc: h3=":443"; ma=2592000,h3=":443"; ma=2592000 cache-control: public, max-age=600 content-type: text/html; charset=utf-8 date: Sun, 28 Dec 2025 15:13:49 GMT etag: "0a0accd457a7b092f908d38ffdc2e5fc97931c28" last-modified: Wed, 29 Oct 2025 20:33:26 GMT referrer-policy: strict-origin-when-cross-origin server: git-pages (git-pages) server: pages-server strict-transport-security: max-age=63072000; includeSubdomains; preload via: 1.1 Caddy content-length: 20342 Cheng Zhang

I am an assistant professor at Worcester Polytechnic Institute (WPI). Previously, I was a postdoc research fellow at UCL Programming Principles, Logic, and Verification Group, working with Professor Alexandra Silva. I have a Ph.D. in computer science from Boston University supervised by Professor Marco Gaboardi. I obtained my bachelor's degree in Mathematics at Wheaton College (MA), advised by Professor William Bloch, and did my honor thesis in graph theory with Professor Rochelle Leibowitz.

My research interests span the theory and practice of programming language and verification across various domains.

The theoretical side of me loves exploring the behaviors of real-world systems through the lenses of coalgebra, Kleene algebra, universal algebra, iteration theory, and category theory. The practical side of me seeks to design efficient, robust, and human-centric verification frameworks that are grounded in solid mathematical principles.

News

Sep 2025 --- I joined Worcester Polytechnic Institute as an assistant professor!

Apr 2025 --- I will be attending SYCO 13 at UCL!

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!

Conference Publications

Outruning Big KATs: Efficient Decision Procedures for Variants of GKAT
with Qiancheng Fu, Ji Hang, Ines Santacruz, Alexandra Silva, Marco Gaboardi
[implementation] (Submitted To POPL 2026)
CF-GKAT: Efficient Validation of Control-Flow Transformations
with Tobias Kappé, David E. Narváez, Nico Naus
[arxiv] [doi] Principles of Programming Languages (POPL 2025)
Kleene Algebra with Commutativity Conditions is Undecidable
with Arthur Azevedo de Amorim, Marco Gaboardi
[arxiv] [hal] [doi] Computer Science Logic (CSL 2025)
Domain Reasoning In TopKAT
with Arthur Azevedo de Amorim, Marco Gaboardi
[arxiv] [doi] International Colloquium on Automata, Languages, and Programming (ICALP 2024)
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)
Note: The language model in the conference version is unsound with respect to the axioms of TopKAT, which invalidates several important results. This error is fixed in the arXiv version, and acknowledged in "Domain Reasoning in TopKAT" (ICALP 2024) by me and my coauthors. We thank Damien Pous and Jana Wagemaker for pointing out this error.
Lexos 2017: Building Reliable Software in Python
with Weiqi Feng, Emma Steffens, Alvaro de Landaluce, Scott Kleinman, Mark D. LeBlanc
[doi] Conference of Computing Sciences in Colleges (CCSC 2018)

Workshops And Theses

TopKAT: When Algebra Proposes to Program Logic
with Arthur Azevedo de Amorim, Marco Gaboardi
Theory and Practice of Static Analysis (TPSA 2025)
Note: Original talk title is "Domain Reasoning In TopKAT: Reduction and Completeness", but we decided to slightly change the topic based on reviewer feedback.
Two Variants of Kleeen Algebra and Their Applications
Cheng Zhang
Ph.D Thesis 2024
A Dependently Typed Language with Dynamic Equality
with Mark Lemay, Qiancheng Fu, William Blair, Hongwei Xi
[doi] Type-Driven Development (TyDe 2023)
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

Teaching

2020 Fall, CS 320: Principles of Programming Language, with Professor Marco Gaboardi and Lecturer Abbas Attarwala
2020 Summer, CS 111: Introduction to Computer Science 1, with Lecturer 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 Lecturer Abbas Attarwala
2019 Spring, CS 320: Principles 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 poems and lyrics I translated and wrote.

Name Pronunciation

Quotes

Mathematical Methods

What I care most about are definitions. [...] Finding the name took several months. Then it took another two or three years to finally write down the correct definition. [...] But even beyond mere language, we perceive mathematical nature through the lenses given by definitions, and it is critical that the definitions put the essential points into focus. -- Peter Scholze
The very effort for rigor forces us to find out simpler methods of proof. -- David Hilbert
It is impossible to be a mathematician without being a poet in soul. -- Sofia Kovalevskaya
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
I can illustrate the [...] approach with [...] a nut to be opened. The unknown thing to be known appeared to me as some stretch of earth or hard marl, resisting penetration. The sea advances insensibly in silence, nothing seems to happen, nothing moves, the water is so far off you hardly hear it, yet it finally surrounds the resistant substance. -- 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

Funny (but True)

ε-transitions are the null pointers of automata. -- Tiago Ferreira
Algebra is the offer made by the devil to the mathematician. The devil says: "I will give you this powerful machine, it will answer any question you like. All you need to do is give me your soul: give up geometry, and you will have this marvelous machine. -- Michael Atiyah
"Should you just be an algebraist or a geometer?" is like saying "Would you rather be deaf or blind?" -- Michael Atiyah
The Axiom of Choice is obviously true, the Well–ordering theorem is obviously false; and who can tell about Zorn’s Lemma? -- Jerry Bona
@wilbowma I study computers so that I may one day defeat them. -- Max S. New [link]

Original Source | Taken Source