The impact of higher-order state and control effects on local relational reasoning

Derek Dreyer, Georg Neis, Lars Birkedal

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstract

    Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages—languages nearly as complex as ML or Haskell. Much of the recent work in this direction has considered the interesting representation independence principles enabled by the use of local state, but it is also important to understand the principles that powerful features like higher-order state and control effects disable. This latter topic has been broached extensively within the framework of game semantics, resulting in what Abramsky dubbed the “semantic cube”: fully abstract game-semantic characterizations of various axes in the design space of ML-like languages. But when it comes to reasoning about many actual examples, game semantics does not yet supply a useful technique for proving equivalences.
    OriginalsprogEngelsk
    TidsskriftJournal of Functional Programming
    Vol/bind22
    Udgave nummer4-5
    ISSN0956-7968
    StatusUdgivet - 2012

    Emneord

    • Step-indexed Kripke logical relations
    • biorthogonality
    • observational equivalence
    • higher-order state
    • local state
    • first-class continuations
    • exceptions
    • state transition systems

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'The impact of higher-order state and control effects on local relational reasoning'. Sammen danner de et unikt fingeraftryk.

    Citationsformater