Computational interpretations of linear logic allow static control of memory resources: the data produced by the program are endowed through its type with attributes that determine its life cycle. This has promoted numerous investigations into safe introduction of in-place update. Various type systems have been proposed for this aim, but the memory management that promotes linear evaluation does not adequately model the destruction of in-place update. The main achievement of this work is to establish a simple theoretical framework that will allow us to clarify the potential (and limits) of linearity to guarantee the process of transforming a functional program into an imperative one. For this purpose we will introduce a type system called "global" that will model the in-place update as the linear system models the one-time use.

翻译：线性逻辑的计算解释允许对内存资源进行静态控制：程序产生的数据通过其类型被赋予决定其生命周期的属性。这促进了关于安全引入就地更新的众多研究。为实现这一目标，已提出了多种类型系统，但促进线性求值的内存管理未能充分模拟就地更新的销毁过程。本工作的主要成就是建立一个简单的理论框架，以澄清线性在保证将函数式程序转换为命令式程序这一过程中的潜力（与局限）。为此，我们将引入一种称为“全局”的类型系统，该系统将模拟就地更新，正如线性系统模拟一次性使用。