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. © Springer-Verlag Berlin Heidelberg 2003.
CITATION STYLE
Konec̃ný, M. (2003). Functional in-place update with layered datatype sharing. Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Springer Verlag. https://doi.org/10.1007/3-540-44904-3_14
Mendeley helps you to discover research relevant for your work.