Typing with conditions and guarantees for functional in-place update

Michal Konečný*

*Corresponding author for this work

    Research output: Chapter in Book/Published conference outputConference publication

    Abstract

    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.

    Original languageEnglish
    Title of host publicationInternational Workshop on Types for Proofs and Programs
    EditorsH. Geuvers, F. Wiedijk
    PublisherSpringer
    Pages182-199
    Number of pages18
    Volume2646
    ISBN (Electronic)978-3-540-39185-2
    ISBN (Print)978-3-540-14031-3
    DOIs
    Publication statusPublished - 15 Apr 2003
    EventTYPES 2002 - Berg en Dal, Netherlands
    Duration: 24 Apr 200228 Apr 2002

    Publication series

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

    Conference

    ConferenceTYPES 2002
    Country/TerritoryNetherlands
    CityBerg en Dal
    Period24/04/0228/04/02

    Fingerprint

    Dive into the research topics of 'Typing with conditions and guarantees for functional in-place update'. Together they form a unique fingerprint.

    Cite this