5 papers
Classifying Capabilities (Extended Version)
Cao Nguyen Pham, Oliver BraÄevac, Yichen Xu +2
Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kin…
LACUNA: Safe Agents as Recursive Program Holes
Yaoyu Zhao, Yichen Xu, Oliver BraÄevac +3
LLM agents increasingly act by writing code, yet a split persists between the runtime that drives the agent and the code the model writes. The runtime owns the loop, context, and c…
Tracking Capabilities for Safer Agents
Martin Odersky, Yaoyu Zhao, Yichen Xu +2
AI agents that interact with the real world through tool calls pose fundamental safety challenges: agents might leak private information, cause unintended side effects, or be manip…
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,…
What's in the Box: Ergonomic and Expressive Capture Tracking over Generic Data Structures (Extended Version)
Yichen Xu, Oliver BraÄevac, Cao Nguyen Pham +1
Capturing types in Scala unify static effect and resource tracking with object capabilities, enabling lightweight effect polymorphism with minimal notational overhead. However, the…