2 citations · 2 across the 7 of their papers we have counts for
5 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…
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…
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…