Functional In-place Update with Layered Datatype Sharing

Michal Konečný, Proceedings of TLCA 2003, Valencia, LNCS 2701, pp 195-210

An older but more detailed version is available as a technical report.

An implementation is available through a web interface .


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).
Michal Konečný
Last modified: Tue Jul 1 11:00:54 BST 2003