Scala中的对象能力和轻量级亲和力：实现、形式化和合理性
Object Capabilities and Lightweight Affinity in Scala: Implementation, Formalization, and Soundness
摘要：
别名是命令式面向对象语言中的一个已知的挑战源，这导致了类型系统在别名控制方面的重要进步。然而，它们的大规模采用已经被证明是一个令人惊讶的困难挑战。虽然新的语言设计显示出了希望，但它们并没有解决现有语言中的别名控制需求。本文提出了一种新的方法来隔离和唯一性在现有的，广泛使用的语言，Scala。这种方法是独一无二的，它解决了采用类型系统扩展进行别名控制的一些最重要的障碍。首先，现有代码的适应只需要最少的注释集。每个类只需要一位信息。令人惊讶的是，该文件表明，这些信息可以提供的对象能力的纪律，广泛使用的程序安全。我们形式化我们的方法作为一个类型系统，并证明关键的可靠性定理。类型系统是为完整的Scala语言实现的，第一次提供了与Scala本地类型推断的良好集成。最后，我们根据经验评估了现有Scala开源代码在超过75，000 KB的语料库上的一致性。
英文摘要：
Aliasing is a known source of challenges in the context of imperative object-oriented languages, which have led to important advances in type systems for aliasing control. However, their large-scale adoption has turned out to be a surprisingly difficult challenge. While new language designs show promise, they do not address the need of aliasing control in existing languages. This paper presents a new approach to isolation and uniqueness in an existing, widely-used language, Scala. The approach is unique in the way it addresses some of the most important obstacles to the adoption of type system extensions for aliasing control. First, adaptation of existing code requires only a minimal set of annotations. Only a single bit of information is required per class. Surprisingly, the paper shows that this information can be provided by the object-capability discipline, widely-used in program security. We formalize our approach as a type system and prove key soundness theorems. The type system is implemented for the full Scala language, providing, for the first time, a sound integration with Scala's local type inference. Finally, we empirically evaluate the conformity of existing Scala open-source code on a corpus of over 75,000 LOC.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
