7 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…
System Capybara: Tracking Capabilities for Separation and Freshness (Extended Version)
Yichen Xu, Oliver BraÄevac, Cao Nguyen Pham +2
Substructural type systems give strong static control over aliasing. Examples include uniqueness, separation, and borrowing. How can such control be brought to established language…
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…
First-Class Refinement Types for Scala
Matt Bovel, Viktor KunÄak, Martin Odersky
Refinement types -- types qualified with logical predicates -- have proven effective for lightweight verification in languages like Liquid Haskell, F*, and Dafny. However, in these…
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…
Agentic Proof Automation: A Case Study
Yichen Xu, Martin Odersky
Proof engineering is notoriously labor-intensive: proofs that are straightforward on paper often require lengthy scripts in theorem provers. Recent advances in large language model…