Typing with conditions and guarantees for functional in-place update

Hofmann's LFPL is a functional language with constructs that can be interpreted as referring to heap locations. In this view, the language is suitable for expressing and verifying in-place update algorithms. Correctness of in-place evaluation is guaranteed by a linear typing. As linearity prevents sharing on the heap, LFPL rejects many sound, natural in-place update algorithms with sharing. Recently, Aspinall and Hofmann added usage aspects to parameters of terms in first-order LFPL in order to type-check sound non-linear programs. Nevertheless, soundness of this system has not been fully established. We show a more subtle meaning of the usage aspects as pre-conditions and (rely-)guarantees about the heap layout before and after evaluation. This interpretation allows a manageable proof of soundness for Aspinall and Hofmann's system. Secondly, we present an algorithm for inferring the strongest sound usage aspects for typable recursive programs. We outline two other annotated typings of LFPL as systems inferring preconditions and (rely-)guarantees, both extending usage aspects. One is Atkey's system based on explicit indication of sharing among parameters in typing contexts and the other one is a system by the author which admits LFPL programs in which datatypes share at different layers. The latter is based on the author's conditions-and-guarantces approach to usage aspects.