一句话：提出 System F<:M，将引用不可变性作为 System F<: 的简单扩展，并证明其安全。
引用不可变性是一种基于类型的技术，用于限制对象突变，长期在 Java 等面向对象语言中研究。但 Scala 等语言模糊了函数式与面向对象语言的边界，因此需要理解引用不可变性如何与高阶函数、多态和子类型等混合语言特性交互。本文构造了演算 System F<:M，将引用不可变性系统编码为 System F<: 的简单扩展，并给出其类型规则与语义。作者证明该演算满足标准的类型可靠性（soundness）以及不可变性安全性质，表明该扩展在保留多态与子类型的同时能安全地追踪引用可变性。
Reference immutability is a type based technique for taming mutation that has long been studied in the context of object-oriented languages, like Java. Recently, though, languages like Scala have blurred the lines between functional programming languages and object oriented programming languages. We explore how reference immutability interacts with features commonly found in these hybrid languages, in particular with higher-order functions – polymorphism – and subtyping. We construct a calculus System F<:M which encodes a reference immutability system as a simple extension of System F<: and prove that it satisfies the standard soundness and immutability safety properties.
@article{paperbot1883,
title = {Simple Reference Immutability for System F
<sub><:</sub>},
author = {Edward Lee and Ondřej Lhoták},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {OOPSLA2},
year = {2023},
doi = {10.1145/3622828}
}