8 papers
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…
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 "…
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…
Let Functions Speak: Lightweight Parametric Polymorphism via Domain and Range Types
Siyuan He, Songlin Jia, Tiark Rompf
Subtyping allows polymorphism at a low price: a concise type such as Int -> Top covers every function that accepts an integer, whatever it returns, whereas the parametric alternati…
Adaptive Proof Refinement with LLM-Guided Strategy Selection
Minghai Lu, Zhe Zhou, Danning Xie +3
Formal verification via theorem proving enables the expressive specification and rigorous proof of software correctness, but it is difficult to scale due to the significant manual…
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…