  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.
