4 papers · 1 filter
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…
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…
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…