System F-sub中的简单引用不可变性
摘要：引用不可变性是一种基于类型的技术，用于控制变异，长期以来一直在面向对象的语言（例如Java）的上下文中研究。然而，最近，像Scala这样的语言模糊了函数式编程语言和面向对象编程语言之间的界限。我们探讨了引用不可变性与这些混合语言中常见特性的相互作用，特别是与高阶函数、多态和子类型化的相互作用。我们构建了一个名为System F-sub-M的计算方式，它将引用不可变性系统编码为F-sub的简单扩展，并证明它满足标准的合理性和不可变性安全性属性。
作者：Edward Lee and Ondv{r}ej Lhot''ak
论文ID：2307.04960
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-12