一句话：提出用余效应跟踪命令式程序中的变量共享，并扩展类型系统以简洁建模唯一性与不可变性。
类型与余效应系统通过变量注解刻画上下文的使用方式，余效应自底向上经代数算子组合。本文表明该原则可用于命令式范式中的共享跟踪，即执行中可能引入的变量间链接，并给出非结构余效应的重要实例：变量使用方式会影响其他变量的余效应，故不能逐变量计算。作者在跟踪共享的类型系统中加入与唯一性和不可变性相关的若干特性，借助余效应方法简洁表达这些特性，并用标准技术证明相关性质。
In type-and-coeffect systems , contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bottom-up, combining, for each term, the coeffects of its subterms, through a fixed set of algebraic operators. We show that this principled approach can be adopted to track sharing in the imperative paradigm, that is, links among variables possibly introduced by the execution. This provides a significant example of non-structural coeffects, which cannot be computed by-variable, since the way a given variable is used can affect the coeffects of other variables. To illustrate the effectiveness of the approach, we enhance the type system tracking sharing to model a sophisticated set of features related to uniqueness and immutability. Thanks to the coeffect-based approach, we can express such features in a simple way and prove related properties with standard techniques.
@article{paperbot1447,
title = {Coeffects for sharing and mutation},
author = {Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca and Marco Servetto},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563319}
}