-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
398 lines (368 loc) · 16.8 KB
/
index.html
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
<!DOCTYPE html>
<html lang="en">
<head>
<meta charset="UTF-8">
<meta name="viewport" content="width=device-width, initial-scale=1.0">
<meta http-equiv="X-UA-Compatible" content="ie=edge">
<meta name="description"
content="Postdoc researcher at UCL, interested in the theory and practice of (co)algebraic method in verification, semantics, and programming language in general.">
<title>Cheng Zhang</title>
<link rel="preconnect" href="https://fonts.googleapis.com">
<link rel="preconnect" href="https://fonts.gstatic.com" crossorigin>
<link
href="https://fonts.googleapis.com/css2?family=Inter:ital,opsz,wght@0,14..32,100..900;1,14..32,100..900&display=swap"
rel="stylesheet">
<link rel="stylesheet" href="https://cdnjs.cloudflare.com/ajax/libs/font-awesome/6.6.0/css/all.min.css">
<link rel="shortcut icon" href="./cat.PNG" />
<link rel="stylesheet" href="./general.css">
</head>
<style>
#header {
margin-top: 20px;
}
#menu-bar {
margin-bottom: 15px;
display: flex;
flex-direction: row;
flex-wrap: wrap;
}
.menu-item,
.menu-divider {
padding: 5px;
white-space: nowrap;
align-self: center;
}
.header-image {
float: right;
width: 30%;
min-width: 150px;
max-width: 300px;
}
.header-image>img {
width: 100%;
}
#news-items {
font-size: large;
margin-left: 50px;
}
@media screen and (max-width: 700px) {
#news-items {
margin-left: 0;
}
}
.description-item {
padding: 10px 0
}
.publication {
list-style-type: disc;
padding: 10px;
}
.publication a {
text-decoration: none;
}
.publication .title {
font-weight: bold;
}
.publication .conference {
font-style: italic;
color:cadetblue;
}
#quotes-list li {
padding-bottom: 10px;
}
</style>
<body>
<div id="all">
<div id="header">
<h1 style="margin:0; padding-right: 10px;display: inline;">Cheng Zhang</h1>
<div style="display: inline; white-space: nowrap;">(he/him)</div>
</div>
<div id="menu-bar">
<a class="menu-item" href="https://media.githubusercontent.com/media/czhang03/CV/master/CV.pdf" target="_blank"
rel="noopener noreferrer"><i class="fa-solid fa-file"></i> CV</a>
<span class="menu-divider">|</span>
<a class="menu-item" href="https://scholar.google.com/citations?user=_pppqNwAAAAJ&hl=en&oi=sra" target="_blank"
rel="noopener noreferrer"><i class="fa-brands fa-google-scholar"></i> Scholar</a>
<span class="menu-divider">|</span>
<a class="menu-item" href="https://www.researchgate.net/profile/Cheng-Zhang-232" target="_blank"
rel="noopener noreferrer"><i class="fa-brands fa-researchgate"></i> ResearchGate</a>
<span class="menu-divider">|</span>
<a class="menu-item" href="mailto:[email protected]" target="_blank" rel="noopener noreferrer"><i
class="fa-solid fa-envelope"></i> [email protected]</a>
<span class="menu-divider">|</span>
<a class="menu-item" href="https://github.com/czhang03/" target="_blank" rel="noopener noreferrer"><i
class="fa-brands fa-github"></i> czhang03</a>
<span class="menu-divider">|</span>
<a class="menu-item" rel="me" href="https://mathstodon.xyz/@czhang03" target="_blank"><i
class="fa-brands fa-mastodon"></i> [email protected]</a>
<span class="menu-divider">|</span>
<a class="menu-item" href="https://signal.me/#eu/pSDabtHXvjldju9PhhotkBJdtdbybXk9TYToSZepoGCTp0ztqMlP1p_Zx3XC9fG1"
target="_blank" rel="noopener noreferrer"><i class="fa-brands fa-signal-messenger"></i> czhang03.04</a>
</div>
<figure class="header-image">
<img src="./photo_cheng.jpeg" alt="Photo of me enjoying some Wendy's spicy chicken nuggets">
<figcaption>
Photo of me enjoying some Wendy's spicy chicken nuggets (not sponsored)
</figcaption>
</figure>
<div class="description-item">
<div>
<p>
I am a postdoc research fellow at UCL
<a href="http://pplv.cs.ucl.ac.uk/" target="_blank" rel="noopener noreferrer">Programming Principles, Logic,
and Verification Group</a>,
working with Professor
<a href="https://alexandrasilva.org" target="_blank" rel="noopener noreferrer">Alexandra Silva</a>.
Prior to that, I was a Ph.D. student at Boston University supervised by Professor
<a href="https://cs-people.bu.edu/gaboardi/" target="_blank" rel="noopener noreferrer">Marco Gaboardi</a>.
</p>
<p>
My works range over a spectrum of practical and theoretical problems in the field of <strong>Kleene
Algebra</strong>.
<ul>
<li>
<strong>On the practical side</strong>, 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.
</li>
<li>
<strong>On the theoretical side</strong>, I am interested in producing simple and elegant proofs
of complicated results like completeness and decidability.
Many of my theoretical work is built upon beautiful ideas from universal algebra,
coalgebra, and category theory.
</li>
</ul>
</p>
<p>You can find out more about my research, teaching, and experiences in
my <a href="https://media.githubusercontent.com/media/czhang03/Research-Statement/main/main.pdf"
target="_blank" rel="noopener noreferrer"><strong>research statement</strong></a>,
<a href="https://media.githubusercontent.com/media/czhang03/teaching-statement/refs/heads/master/main.pdf"
target="_blank" rel="noopener noreferrer"><strong>teaching statement</strong></a>,
<a href="https://media.githubusercontent.com/media/czhang03/DEI-Statement/refs/heads/main/main.pdf"
target="_blank" rel="noopener noreferrer"><strong>DEI statement</strong></a>, and
<a href="https://media.githubusercontent.com/media/czhang03/CV/master/CV.pdf" target="_blank"
rel="noopener noreferrer"><strong>CV</strong></a>.
</p>
</div>
</div>
<div class="description-item">
<h2>News</h2>
<div id="news-items">
<p><strong>Nov 2024</strong> --- Our paper "CF-GKAT: Efficient Validation of Control-Flow
Transformations" is accepted at <a href="https://conf.researchr.org/home/POPL-2025"
target="_blank" rel="noopener noreferrer">POPL 2025</a>.
Hope to see you in Denver, Colorado!</p>
<p><strong>Oct 2024</strong> --- Our paper "Kleene algebra with commutativity conditions is undecidable" is
accepted at <a href="https://csl2025.github.io/" target="_blank" rel="noopener noreferrer">CSL 2025</a>.</p>
<p><strong>Oct 2024</strong> --- I have joined <a href="http://pplv.cs.ucl.ac.uk/welcome/" target="_blank"
rel="noopener noreferrer">PPLV groups</a> of UCL as a postdoc! I am honored to work with <a
href="https://alexandrasilva.org/#/main.html" target="_blank" rel="noopener noreferrer">Prof. Alexandra
Silva</a>, and her talented group. </p>
<p><strong>Sep 2024</strong> --- I will be attending <a href="https://nepls.org/" target="_blank"
rel="noopener noreferrer">NEPLS</a> 2024 at NEU!</p>
<p><strong>Aug 2024</strong> --- I have finished my Ph.D. at Boston University! </p>
</div>
</div>
<div class="description-item">
<h2>Conference Publications</h2>
<ul>
<li class="publication">
<span class="title">Symbolic On-the-fly Algorithms For GKAT Equivalence</span>
<br>
<span class="author">with Qiancheng Fu, Ji Hang, Ines Santacruz, Marco Gaboardi </span>
<br>
[<a href="https://github.com/qcfu-bu/rust-gkat" target="_blank" rel="noopener noreferrer">implementation</a>]
<span class="conference">(Submitted To LICS 2025)</span>
</li>
<li class="publication">
<span class="title">CF-GKAT: Efficient Validation of Control-Flow
Transformations</span>
<br>
<span class="author">with Tobias Kappé, David E. Narváez, Nico Naus </span>
<br>
[<a href="https://arxiv.org/abs/2411.13220" target="_blank" rel="noopener noreferrer">arxiv</a>]
[<a href="https://doi.org/10.1145/3704857" target="_blank" rel="noopener noreferrer">doi</a>]
<span class="conference">
Principles of Programming Languages (POPL 2025)
</span>
</li>
<li class="publication">
<span class="title">Kleene Algebra with Commutativity Conditions is Undecidable</span>
<br>
<span class="author">with Arthur Azevedo de Amorim, Marco Gaboardi</span>
<br>
<span>
[<a href="https://arxiv.org/abs/2411.15979" target="_blank" rel="noopener noreferrer">arxiv</a>]
[<a href="https://hal.science/hal-04534715/" target="_blank" rel="noopener noreferrer">hal</a>]
[<a href="https://doi.org/10.4230/LIPIcs.CSL.2025.36" target="_blank" rel="noopener noreferrer">doi</a>]
</span>
<span class="conference">Computer Science Logic (CSL 2025)</span>
</li>
<li class="publication">
<span class="title">Domain Reasoning In TopKAT</span>
<br>
<span class="author">with Arthur Azevedo de Amorim, Marco Gaboardi</span>
<br>
<span>
[<a href="https://arxiv.org/abs/2404.18417" target="_blank" rel="noopener noreferrer">arxiv</a>]
[<a href="https://doi.org/10.4230/LIPIcs.ICALP.2024.157" target="_blank" rel="noopener noreferrer">doi</a>]
</span>
<span class="conference">International Colloquium on Automata, Languages, and Programming (ICALP 2024)</span>
</li>
<li class="publication">
<span class="title">On Incorrectness Logic and Kleene Algebra With Top and Tests</span>
<br>
<span class="author">with Arthur Azevedo de Amorim, Marco Gaboardi</span>
<br>
<span>
[<a href="https://arxiv.org/abs/2108.07707" target="_blank" rel="noopener noreferrer">arxiv</a>]
[<a href="https://doi.org/10.1145/3498690" target="_blank" rel="noopener noreferrer">doi</a>
(<strong>contains errors</strong>)]
</span>
<span class="conference">Principles of Programming Languages (POPL 2022)</span>
<p>
<strong>Note:</strong>
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.
</p>
</li>
<li class="publication">
<span class="title">Lexos 2017: Building Reliable Software in Python</span>
<br>
<span class="author"> with Weiqi Feng, Emma Steffens, Alvaro de Landaluce, Scott Kleinman, Mark D.
LeBlanc </span>
<br>
<span>
[<a href="https://dl.acm.org/doi/10.5555/3205191.3205205" target="_blank" rel="noopener noreferrer">doi</a>]
</span>
<span class="conference">Conference of Computing Sciences in Colleges (CCSC 2018)</span>
</li>
</ul>
</div>
<div class="description-item">
<h2>Workshops And Theses</h2>
<ul>
<li class="publication">
<span class="title">TopKAT: When Algebra Proposes to Program Logic</span>
<br>
<span class="author">with Arthur Azevedo de Amorim, Marco Gaboardi</span>
<br>
<span class="conference">Theory and Practice of Static Analysis (TPSA 2025)</span>
<p>
<strong>Note:</strong>
Original talk title is "Domain Reasoning In TopKAT: Reduction and Completeness",
but we decided to slightly change the topic based on reviewer feedback.
</p>
</li>
<li class="publication">
<span class="title">Two Variants of Kleeen Algebra and Their Applications</span>
<br>
<span class="author">Cheng Zhang</span>
<br>
<span class="conference">Ph.D Thesis 2024</span>
</li>
<li class="publication">
<span class="title">A Dependently Typed Language with Dynamic Equality</span>
<br>
<span class="author">with Mark Lemay, Qiancheng Fu, William Blair, Hongwei Xi</span>
<br>
<span>
[<a href="https://dl.acm.org/doi/10.1145/3609027.3609407" target="_blank" rel="noopener noreferrer">doi</a>]
</span>
<span class="conference">Type-Driven Development (TyDe 2023)</span>
</li>
<li class="publication">
<span class="title"> Developing a Dependently Typed Language with Runtime Proof Search (Extended
Abstract)</span>
<br>
<span class="author">with Mark Lemay, William Blair</span>
<br>
<span>
[<a
href="https://icfp20.sigplan.org/details/tyde-2020-papers/7/Developing-a-Dependently-Typed-Language-with-Runtime-Proof-Search-Extended-Abstract-"
target="_blank" rel="noopener noreferrer">ICFP website</a>]
</span>
<span class="conference">Type-Driven Development (TyDe 2020)</span>
</li>
<li class="publication">
<span class="title">Kings in Generalized Tournaments</span>
<br>
<span class="author">Cheng Zhang</span>
<br>
<span>
[<a href="http://hdl.handle.net/11040/24570" target="_blank" rel="noopener noreferrer">archive</a>]
</span>
<span class="conference">Undergraduate Honor Thesis 2018</span>
</li>
</ul>
</div>
<div class="description-item">
<h2>Teaching</h2>
<div>
<ul>
<li>2020 Fall, CS 320: Principles of Programming Language,
with Professor Marco Gaboardi and Lecturer Abbas Attarwala</li>
<li>2020 Summer, CS 111: Introduction to Computer Science 1,
with Lecturer John Magee</li>
<li>2020 Summer, CS 112: Introduction to Computer Science 2,
with Lecturer Christine Papadakis-Kanaris</li>
<li>2020 Spring, CS 235: Algebraic Algorithm,
with Professor Leonid Levin</li>
<li>2019 Fall, CS 132: Geometric Algorithm,
with Lecturer Abbas Attarwala</li>
<li>2019 Spring, CS 320: Principles of Programming Language,
with Professor Wayne Snyder</li>
</ul>
</div>
</div>
<div class="description-item">
<h2>Hobbies</h2>
<div>
<p>
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 href="./blogs/">a tiny blog</a> of some poems and lyrics I translated and wrote.
These translations are generally terrible, but I am trying to get better.
</p>
</div>
</div>
<div class="description-item">
<h2>Name Pronunciation</h2>
<div>
<embed width='375' height='180' style="display: inline;"
src='https://embed.howtopronounce.com/classic/en/cheng-zhang/31025465'>
</div>
</div>
<div class="description-item"></div>
<h2>Quotes</h2>
<ul id="quotes-list">
<li>
<em> 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.</em>
-- Alexander Grothendieck
</li>
<li>
<em> 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. </em>
-- Edsger W. Dijkstra
</li>
<li>
<em>Either mathematics is too big for the human mind, or the human mind is more than a machine.</em>
-- Kurt Gödel
</li>
<li>
<em>It is impossible to be a mathematician without being a poet in soul.</em>
-- Sofia Kovalevskaya
</li>
<li>
<em>@wilbowma I study computers so that I may one day defeat them</em>
-- Max S. New [<a href="https://types.pl/@maxsnew/112510048499095810" target="_blank" rel="noopener noreferrer">link</a>]
</li>
</ul>
</div>
</body>
</html>