5 papers · 1 filter
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…
Free to Move: Reachability Types with Flow-Sensitive Effects for Safe Deallocation and Ownership Transfer
Haotian Deng, Siyuan He, Songlin Jia +2
We present a flow-sensitive effect system for reachability types that supports explicit memory management, including Rust-style move semantics, in higher-order impure functional la…
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…
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…