Runming Li
where else to find them
what they talk about
where they keep going back
no series more than once — all 2 in the filters
on a stage with
all 5 in the filters
who talks about the same things
- David M. Kahn2 talks
- Jan Hoffmann9 talks
- Di Wang12 talks
- Jonathan Aldrich17 talks
- Jason Z. S. Hu6 talks
- Philip Wadler14 talks
| title | conference | date |
|---|---|---|
| Mechanizing Synthetic Tait Computability in Istari | CPP 2026 | 2026-01-12 |
Mechanization of Synthetic Tait Computability is formalized in the Istari extensional type theory with equality reflection, producing a reusable library of… | ||
| Abstraction Functions as Types | POPL 2026 | 2026-01-11 |
Encodes abstraction functions inside types by adding a single new proposition (an abstract phase) to univalent dependent type theory, then uses a gluing… | ||
| Big-Stop Semantics: Small-Step Semantics in a Big-Step Judgment | POPL 2026 | 2026-01-11 |
Extends big-step semantics with a nondeterministic big-stop rule schema that captures every finite prefix of diverging small-step runs, proving equivalence to… | ||
| nothing matches | ||