Hofmann's LFPL is a functional language with constructs which 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 this semantics is achieved by a linear typing. We introduce a non-linear typing of first-order LFPL programs which is more permissive than the recent effect-based typing of Aspinall and Hofmann. The system efficiently infers separation assertions as well as destruction and re-use effects for individual layers of recursive-type values. Thus it is suitable for in-place update algorithms with complicated data aliasing.
BibTeX pdf(a4), ps.gz(a4).