AI 中文总结
研究如何将子结构类型系统的别名控制引入Scala，开发系统水豚，通过跟踪能力相关特性恢复关键原则，给出保类型翻译并证明语义健全性，实现Scala 3新分离检查器，带来高阶分离推理。
AI 中文摘要
子结构类型系统对别名提供强大的静态控制，如唯一性、分离和借用。对于依赖高阶抽象、无限制别名和广泛共享的现有语言，如何引入这种控制？本文在Scala环境下研究该问题，展示如何有选择地而非全局地改造这些保证。从Scala的捕获检查出发，开发了系统水豚，通过跟踪能力的分离、消耗、新鲜度和只读访问，恢复了关键推理原则。给出从表面演算到核心演算的保类型翻译，证明了核心演算的语义健全性，实现了Scala 3的新分离检查器。
英文摘要
Substructural type systems give strong static control over aliasing. Examples include uniqueness, separation, and borrowing. How can such control be brought to established languages whose programming models rely on higher-order abstraction, unrestricted aliasing, and pervasive sharing? We study this problem in the context of Scala. We show how to retrofit these guarantees selectively instead of globally: ordinary code keeps Scala's usual aliasing discipline, while stronger guarantees can be enforced where they matter. Our starting point is Scala's capture checking, whose treatment of capabilities is inspired by the object-capability tradition: capabilities are ordinary values, and capture sets record, in a value's type, which capabilities the value may use. We develop System Capybara, which adds a selective alias-control layer to this mechanism. By tracking separation, consumption, freshness, and read-only access for capabilities, Capybara recovers key reasoning principles from substructural and ownership-based disciplines without global invariants. We give a type-preserving translation from the surface calculus Capybara to CoreCapybara, a core calculus extending System Capless, the earlier foundation for capture checking. The translation uses quantifiers for capture polymorphism and freshness, and constraint-indexed modal types for separation. We prove a semantic soundness result for the core calculus in Lean 4 and derive type safety, memory safety (no use-after-free or double-free), immutability of read-only computations, and data-race freedom for well-typed programs. Finally, we implement Scala 3's new separation checker, which brings higher-order separation reasoning about effects, capabilities, and resources to ordinary Scala, including fearless concurrency.
