2 citations · 5 across the 7 of their papers we have counts for
9 papers
Towards Definitional Interpreters for Hoare Logics
Ke Sun, Di Wang, Yuyan Bao +2
Intrinsic definitional interpreters, definitional interpreters that operate on typing derivations instead of abstract syntax trees, have recently been studied as a promising method…
Capture Now, Consume Later: Reachability Types with Flow-Sensitive Effects for Higher-Order Ownership Transfer
Haotian Deng, Siyuan He, Songlin Jia +2
Higher-order impure programs routinely transfer or consume a resource through a closure: when one access path consumes the resource, it must be disabled through all remaining alias…
Type, Ability, and Effect Systems: Perspectives on Purity, Semantics, and Expressiveness
Yuyan Bao, Tiark Rompf
Programming benefits from a clear separation between pure, mathematical computation and impure, effectful interaction with the world. Existing approaches to enforce this separation…
Typestate via Revocable Capabilities
Songlin Jia, Craig Liu, Siyuan He +3
Managing stateful resources safely and expressively is a longstanding challenge in programming languages, especially in the presence of aliasing. For example, scope-based construct…
When Lifetimes Liberate: A Type System for Arenas with Higher-Order Reachability Tracking
Siyuan He, Songlin Jia, Yuyan Bao +1
Static resource management in languages remains challenging due to tensions among control, expressiveness, and flexibility. Region-based systems [Grossman et al . 2002; Tofte et al…
Complete the Cycle: Reachability Types with Expressive Cyclic References (Extended Version)
Haotian Deng, Siyuan He, Songlin Jia +2
Local reasoning about programs that combine aliasing and mutable state is a longstanding challenge. Existing approaches -- ownership systems, linear and affine types, uniqueness ty…
Escape with Your Self: Sound and Expressive Bidirectional Typing with Avoidance for Reachability Types
Songlin Jia, Guannan Wei, Siyuan He +2
Reasoning about programs in the presence of mutation and aliasing is notoriously difficult. Rust has popularized lifetime-based ownership tracking in systems programming, but its "…
Graph IRs for Impure Higher-Order Languages (Technical Report)
Oliver Bračevac, Guannan Wei, Songlin Jia +4
This is a companion report for the OOPSLA 2023 paper of the same title, presenting a detailed end-to-end account of the graph IR, at a level of detail beyond a r…
Modeling Reachability Types with Logical Relations
Yuyan Bao, Songlin Jia, Guannan Wei +2
Reachability types are a recent proposal to bring Rust-style reasoning about memory properties to higher-level languages, with a focus on higher-order functions, parametric types,…