Yizhou Zhang
where else to find them
no profile links on file
what they talk about
where they keep going back
- PLDI Workshop Honoring Andreas Podelski4 editions2023–2026
- OOPSLA3 editions2020–2025
- POPL2 editions2022–2023
all 6 in the filters
on a stage with
all 20 in the filters
who talks about the same things
- Jianlin Li3 talks
- Steve Zdancewic19 talks
- Nada Amin26 talks
- Zhenjiang Hu15 talks
- Nicolas Wu25 talks
- Tiark Rompf24 talks
| title | conference | date |
|---|---|---|
| Virtualizing Continuations | PLDI 2026 | 2026-06-15 |
Implements a novel virtual continuation scheme that assigns virtual addresses to stack-allocated handlers and mediates effect invocations via a software MMU… | ||
| Zero-Overhead Lexical Effect Handlers | OOPSLA 2025 | 2025-10-16 |
Claims a zero-overhead implementation for lexically scoped exceptional effect handlers via a type-directed translation that emits static provenance metadata… | ||
| Compiling with Generating Functions | ICFP 2025 | 2025-10-12 |
A compiler called Genie compiles probabilistic programs to generating functions as a deterministic target (PIL → DIL) and proves correctness against a… | ||
| Language Design Where Paradigms Meet | PLMW @ PLDI 2025 | 2025-06-16 |
A new language called rocket extends rock with object‑oriented abstractions so inductive types and proofs are open inductive types that late‑bind constructors… | ||
| Certified Compilers à la Carte | PLDI 2025 | 2025-06-16 |
The work extends the Rocq proof assistant with a plugin called Rocqet that adds object-oriented extensibility features—late binding, mixin composition, and… | ||
| Semantics of the memo Probabilistic Programming Language | LAFI 2025 | 2025-01-19 |
Formal semantics for the memo probabilistic programming language claim: a frame of mind is the core state that records choices, subframes and equations and… | ||
| Lexical Effect Handlers, Directly | OOPSLA 2024 | 2024-10-20 |
Compiles lexically scoped algebraic effect handlers down to low-level stack switching and header frames, identifying handlers by memory address so handler… | ||
| Persimmon: Nested Family Polymorphism with Extensible Variant Types | OOPSLA 2024 | 2024-10-20 |
Persimmon implements nested family polymorphism with extensible variant types, using a linkage concatenation representation to combine inherited and new… | ||
| Compiling Probabilistic Programs for Variable Elimination with Information Flow | PLDI 2024 | 2024-06-24 |
This paper presents a compiler, Maple, that uses an information-flow type system to partition and eliminate discrete latent variables in recursive… | ||
| Extensible Metatheory Mechanization via Family Polymorphism | PLDI 2023 | 2023-06-17 |
Claims a language-layer for family polymorphism inside Coq that reuses code and proofs via late binding and generates a Coq plugin plus a core dependent type… | ||
| Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortize... | POPL 2023 | 2023-01-15 |
An automatic guide synthesizer generates neural-guide programs by a type-preserving, dependence-aware translation that guarantees mutual absolute continuity… | ||
| Reasoning about 'Reasoning about Reasoning' Semantics and Contextual Equivalence | POPL 2022 | 2022-01-16 |
Formal semantics for a core PPL with continuous distributions, scoring, nested queries and general recursion defines mutually recursive semantics so… | ||
| Handling Bidirectional Control Flow | OOPSLA 2020 | 2020-11-15 |
Claims that algebraic effects can themselves raise effects and still be statically safe, implemented as a core calculus and type system that forbids unhandled… | ||
| nothing matches | ||