Hoare type theory, polymorphism and separation

Alexandar Nanevski, J. Gregory Morrisett, Lars Birkedal

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review


    We consider the problem of reconciling a dependently typed functional language with
    imperative features such as mutable higher-order state, pointer aliasing, and nontermination.
    We propose Hoare type theory (HTT), which incorporates Hoare-style specifications into
    types, making it possible to statically track and enforce correct use of side effects.
    The main feature of HTT is the Hoare type {P}x:A{Q} specifying computations with
    precondition P and postcondition Q that return a result of type A. Hoare types can be nested,
    combined with other types, and abstracted, leading to a smooth integration with higher-order
    functions and type polymorphism.
    We further show that in the presence of type polymorphism, it becomes possible to interpret
    the Hoare types in the “small footprint” manner, as advocated by separation logic, whereby
    specifications tightly describe the state required by the computation.
    We establish that HTT is sound and compositional, in the sense that separate verifications
    of individual program components suffice to ensure the correctness of the composite program.
    TidsskriftJournal of Functional Programming
    Udgave nummer5-6
    Sider (fra-til)865-911
    Antal sider47
    StatusUdgivet - 2008