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 linearity and correctness of in-place update are properties that are not fully compatible. 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.

翻译：线性逻辑的计算解释实现了对内存资源的静态控制：程序产生的数据通过其类型赋予的属性决定其生命周期。这推动了对安全引入原地更新的诸多研究。为此目的已提出多种类型系统，但线性性和原地更新的正确性并非完全兼容。本研究的主要成果是建立一个简单的理论框架，使我们能够阐明线性性在保证函数式程序向命令式程序转换过程中的潜力与局限性。