Functional in-place update with layered datatype sharing

Michal Konec̃ný*

*Corresponding author for this work

    Research output: Chapter in Book/Published conference outputConference publication


    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.

    Original languageEnglish
    Title of host publicationInternational Conference on Typed Lambda Calculi and Applications
    Number of pages16
    ISBN (Electronic)978-3-540-44904-1
    ISBN (Print)978-3-540-40332-6
    Publication statusPublished - 27 May 2003

    Publication series

    NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
    ISSN (Print)0302-9743


    Dive into the research topics of 'Functional in-place update with layered datatype sharing'. Together they form a unique fingerprint.

    Cite this