-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathindex.html
266 lines (255 loc) · 13.4 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
<!DOCTYPE html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8" />
<meta http-equiv="Content-Style-Type" content="text/css" />
<title>John Li</title>
<link rel="stylesheet" href="https://fonts.googleapis.com/css?family=Roboto">
<link rel="stylesheet" type="text/css" href="normalize.css" />
<link rel="stylesheet" type="text/css" href="main.css" />
<script src="abstracts.js"></script>
<!-- Google tag (gtag.js) -->
<script async src="https://www.googletagmanager.com/gtag/js?id=G-2LPT4XM85R"></script>
<script>
window.dataLayer = window.dataLayer || [];
function gtag(){dataLayer.push(arguments);}
gtag('js', new Date());
gtag('config', 'G-2LPT4XM85R');
</script>
</head>
<body>
<br>
<img src="photo.jpg" style="width: 10em; margin-left: 1em; float: right">
<h1 class="title">John Li <span style="font-size:50%"><a href="cv.pdf">CV</a></span></h1>
<p>
I'm a PhD student in programming languages working with
<a href="https://www.ccs.neu.edu/home/amal/">Amal Ahmed</a>
and
<a href="https://www.khoury.northeastern.edu/home/sholtzen/">Steven Holtzen</a>
at Northeastern University.
I'm generally interested in logic, semantics, and mechanized proof;
lately I've been thinking about connections between mutable state and probability theory.
Before starting my PhD, I built a verified-optimization-pass generator as
part of the <a href="https://certicoq.org/">CertiCoq</a> project.
When I'm not thinking about research, I like learning math and
playing bullet chess, violin, and <a href="https://sympa.inria.fr/sympa/arc/coq-club/2020-01/msg00095.html">ping pong</a>.
</p>
<br/>
<h3>Papers</h3>
<table class="entries">
<tr>
<td>
A Nominal Approach to Probabilistic Separation Logic
<span class="label">LICS 2024</span>
<br/><small>John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen.</small>
<br/>
<small><a href="#" onclick="toggleAbstract('nominal'); return false;">Abstract</a></small>
<small><a href=a-nominal-approach-to-probabilistic-separation-logic-slides.pdf>Slides</a></small>
<small><a href="https://arxiv.org/abs/2405.06826">arXiv</a></small>
<small><a href=https://dl.acm.org/doi/10.1145/3661814.3662135>DOI</a></small>
<small><a href=a-nominal-approach-to-probabilistic-separation-logic.pdf>Local copy</a></small>
<br/>
<span id="nominal-abstract" class="abstract">
Currently, there is a gap between the tools used by probability
theorists and those used in formal reasoning about probabilistic
programs. On the one hand, a probability theorist decomposes
probabilistic state along the simple and natural product of probability
spaces. On the other hand, recently developed probabilistic separation
logics decompose state via relatively unfamiliar measure-theoretic
constructions for computing unions of sigma-algebras and probability
measures. We bridge the gap between these two perspectives by showing
that these two methods of decomposition are equivalent up to a suitable
equivalence of categories. Our main result is a probabilistic analog of
the classic equivalence between the category of nominal sets and the
Schanuel topos. Through this equivalence, we validate design decisions
in prior work on probabilistic separation logic and create new
connections to nominal-set-like models of probability.
</span>
</td>
</tr>
<tr>
<td>
Lilac: A Modal Separation Logic for Conditional Probability
<span class="label">PLDI 2023</span>
<br/><small>John M. Li, Amal Ahmed, and Steven Holtzen.</small>
<br/>
<small><a href="#" onclick="toggleAbstract('lilac'); return false;">Abstract</a></small>
<small><a href=lilac-slides.pdf>Slides</a></small>
<small><a href="https://arxiv.org/abs/2304.01339">arXiv</a></small>
<small><a href=https://dl.acm.org/doi/10.1145/3591226>DOI</a></small>
<small><a href=lilac-a-modal-separation-logic-for-conditional-probability.pdf>Local copy</a></small>
<small><a href="#" onclick="toggleNotes('lilac'); return false;">Notes</a></small>
<br/>
<span id="lilac-abstract" class="abstract">
We present Lilac, a separation logic for reasoning about probabilistic
programs where separating conjunction captures probabilistic
independence. Inspired by an analogy with mutable state where sampling
corresponds to dynamic allocation, we show how probability spaces over a
fixed, ambient sample space appear to be the natural analogue of heap
fragments, and present a new combining operation on them such that
probability spaces behave like heaps and measurability of random
variables behaves like ownership. This combining operation forms the
basis for our model of separation, and produces a logic with many
pleasant properties. In particular, Lilac has a frame rule identical to
the ordinary one, and naturally accommodates advanced features like
continuous random variables and reasoning about quantitative properties
of programs. Then we propose a new modality based on disintegration
theory for reasoning about conditional probability. We show how the
resulting modal logic validates examples from prior work, and give a
formal verification of an intricate weighted sampling algorithm whose
correctness depends crucially on conditional independence structure.
</span>
<span id="lilac-notes" class="notes">
<p>Since publication, <a href="http://baojia.lu/">Jialu Bao</a>
has pointed out that the interpretation of
almost-sure equality of random variables does not validate
the expected substitution rule, due to a subtle point about
negligibility. This issue is corrected in the local copy above
and on arXiv; see <a href="lilac-a-modal-separation-logic-for-conditional-probability.pdf#page=33">Appendix B.5</a> for details.</p>
<p>We did not attempt to fully mechanize Lilac, but
we do have a mechanization of
our main result that probability spaces
form a Kripke resource monoid (<a href="lilac-a-modal-separation-logic-for-conditional-probability.pdf#page=11">Theorem 2.4</a> in the paper).
See <a href="https://neuppl.khoury.northeastern.edu/blog/2023/pi-lambda/">this blog post</a>
for links to the mechanization, and for a PL-brained presentation of the pi-lambda theorem,
a workhorse of measure-theoretic probability.</p>
</span>
</td>
</tr>
<tr>
<td>
Deriving Efficient Program Transformations from Rewrite Rules
<span class="label">ICFP 2021</span>
<br/><small>John M. Li and Andrew W. Appel.</small>
<br/>
<small><a href="#" onclick="toggleAbstract('deriver'); return false;">Abstract</a></small>
<small><a href=deriving-efficient-program-transformations-from-rewrite-rules-slides.pdf>Slides</a></small>
<small><a href=https://dl.acm.org/doi/10.1145/3473579>DOI</a></small>
<small><a href=deriving-efficient-program-transformations-from-rewrite-rules.pdf>Local copy</a></small>
<br/><span id="deriver-abstract" class="abstract">
An efficient optimizing compiler can perform many cascading rewrites in
a single pass, using auxiliary data structures such as variable binding
maps, delayed substitutions, and occurrence counts. Such optimizers
often perform transformations according to relatively simple rewrite
rules, but the subtle interactions between the data structures needed
for efficiency make them tricky to write and trickier to prove correct.
We present a system for semi-automatically deriving both an efficient
program transformation and its correctness proof from a list of rewrite
rules and specifications of the auxiliary data structures it requires.
Dependent types ensure that the holes left behind by our system (for the
user to fill in) are filled in correctly, allowing the user low-level
control over the implementation without having to worry about getting it
wrong. We implemented our system in Coq (though it could be implemented
in other logics as well), and used it to write optimization passes that
perform uncurrying, inlining, dead code elimination, and static
evaluation of case expressions and record projections. The generated
implementations are sometimes faster, and at most 40% slower, than
hand-written counterparts on a small set of benchmarks; in some cases,
they require significantly less code to write and prove correct.
</span>
</td>
</tr>
<tr>
<td>
Compositional Optimizations for CertiCoq
<span style="float: right">ICFP 2021</span>
<br/><small>Zoe Paraskevopoulou, John M. Li, and Andrew W. Appel.</small>
<br/>
<small><a href="#" onclick="toggleAbstract('certicoq'); return false;">Abstract</a></small>
<small><a href=https://dl.acm.org/doi/10.1145/3473591>DOI</a></small>
<small><a href=compositional-optimizations-for-certicoq.pdf>Local copy</a></small>
<br/><span id="certicoq-abstract" class="abstract">
Compositional compiler verification is a difficult problem that focuses
on separate compilation of program components with possibly different
verified compilers. Logical relations are widely used in proving
correctness of program transformations in higher-order languages;
however, they do not scale to compositional verification of multi-pass
compilers due to their lack of transitivity. The only known technique to
apply to compositional verification of multi-pass compilers for
higher-order languages is parametric inter-language simulations (PILS),
which is however significantly more complicated than traditional proof
techniques for compiler correctness. In this paper, we present a novel
verification framework for <i>lightweight compositional compiler
correctness</i>. We demonstrate that by imposing the additional restriction
that program components are compiled by pipelines that go through <i>the
same sequence of intermediate representations</i>, logical relation proofs
can be transitively composed in order to derive an end-to-end
compositional specification for multi-pass compiler pipelines. Unlike
traditional logical-relation frameworks, our framework supports
divergence preservation---even when transformations reduce the number of
program steps. We achieve this by parameterizing our logical relations
with a pair of <i>relational invariants</i>.
<br/>
<br/>
We apply this technique to verify a multi-pass, optimizing middle-end
pipeline for CertiCoq, a compiler from Gallina (Coq's specification
language) to C. The pipeline optimizes and closure-converts an untyped
functional intermediate language (ANF or CPS) to a subset of that
language without nested functions, which can be easily code-generated to
low-level languages. Notably, our pipeline performs more complex
closure-allocation optimizations than the state of the art in verified
compilation. Using our novel verification framework, we prove an
end-to-end theorem for our pipeline that covers both termination and
divergence and applies to whole-program and separate compilation, even
when different modules are compiled with different optimizations. Our
results are mechanized in the Coq proof assistant.
</span>
</td>
</tr>
</table>
<h3>Extended abstracts</h3>
<table class="entries">
<tr>
<td>
Towards Symbolic Execution for Probability and Non-determinism<span class="label">LAFI @ POPL 2025</span>
<br/><small>Jack Czenszak, John M. Li, Steven Holtzen.</small>
<br/>
<small><a href="lafi25.pdf">Extended Abstract</a></small>
</td>
</tr>
<tr>
<td>
Towards a Categorical Model of the Lilac Separation Logic<span class="label">LAFI @ POPL 2024</span>
<br/><small>John M. Li, Jon Aytac, Philip Johnson-Freyd, Amal Ahmed, and Steven Holtzen.</small>
<br/>
<small><a href="lafi24.pdf">Extended Abstract</a></small>
<small><a href=lafi24-slides.pdf>Slides</a></small>
</td>
</tr>
<tr>
<td>
New Foundations for Probabilistic Separation Logic<span class="label">LAFI @ POPL 2023</span>
<br/><small>John M. Li, Amal Ahmed, and Steven Holtzen.</small>
<br/>
<small><a href="lafi-extended-abstract.pdf">Extended Abstract</a></small>
<small><a href=new-foundations-for-probabilistic-separation-logic.pdf>Slides</a></small>
<small><a href="new-foundations-for-probabilistic-separation-logic-poster.pdf">Poster</a></small>
</td>
</tr>
</table>
<br/>
<br/>
<br/>
<br/>
<br/>
<a href='https://cho.minsung.pl/' style='font-size:1px'>m</a>
<a href='https://olekg.pl/' style='font-size:1px'>o</a>
</body>
</html>