Songlin Jia
where else to find them
no profile links on file
what they talk about
where they keep going back
- OOPSLA3 editions2023–2025
on a stage with
all 9 in the filters
who talks about the same things
- Yuyan Bao8 talks
- Guannan Wei21 talks
- Oliver Bračevac9 talks
- Tiark Rompf24 talks
- Siyuan He2 talks
- Yuxuan Jiang5 talks
| title | conference | date |
|---|---|---|
| Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for(…) | PLDI 2026 | 2026-06-15 |
Presents an algorithmic design for reachability types that proves sound and decidable bidirectional typing and avoidance, mechanized in Lean 4 and accompanied… | ||
| Typestate via Revocable Capabilities | PLDI 2026 | 2026-06-15 |
Presents a Scala 3 compiler extension (prototype in Stella) that implements flow-sensitive revocation, ties capabilities to objects via path-dependent… | ||
| Modeling Reachability Types with Logical Relations -- Semantic Type Soundness,(…) | OOPSLA 2025 | 2025-10-16 |
Presents a formal logical-relations model for reachability types that augments standard relations with relational store typing to localize heap reasoning, and… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in(…) | OOPSLA 2024 | 2024-10-20 |
Presents a type system that adds a freshness qualifier to reachability types so newly allocated values remain distinct until substituted, enabling precise… | ||
| Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in ... | POPL 2024 | 2024-01-14 |
Introduces a new freshness qualifier (diamond) that marks allocations whose reachability may materialize later, and designs two calculi (λ✦ and F✦ calculi)… | ||
| Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Af... | OOPSLA 2023 | 2023-10-23 |
A typed graph IR combines reachability types with an effect system to compute precise, flow-sensitive effect dependencies without CFA by doing type-based… | ||
| nothing matches | ||