Denotational World-indexed Logical Relations and Friends

Jacob Junker Thamsborg

    Publikation: Bog / Antologi / Rapport / Ph.D.-afhandlingPh.d.-afhandling


    As part of the long-standing drive for mathematical machinery to reason about
    computer programs, we use the technique of denotational logical relations to prove
    contextual equivalence of stateful programs. We propose the notion of approximate
    locations to solve the non-trivial problem of existence and solve the fundamental
    type-worlds circularity by metric-space theory. This approach scales to state-of-theart
    step-indexed techniques and permits unrestricted relational reasoning by the use
    of so-called Bohr relations.
    Along the way, we develop auxiliary theory; most notably a generalized version
    of a classical xed-point theorem for functors on certain metric spaces by America
    and Rutten. Also we investigate the use of recursively dened metric worlds in an
    operational setting and arrive at constructions akin to step-indexed models.
    On a dierent, though related, note, we explore a relational reading of separation
    logic with assertion variables. In particular, we give criteria for when standard,
    unary separation logic proofs lift to the binary setting. Phrased dierently, given
    a module-dependent client and a standard separation logic proof of its correctness,
    we ponder the default question of representation-independence: is the client able to
    { or unable to { observe implementation specic details about its module.
    ForlagIT-Universitetet i København
    Antal sider222
    StatusUdgivet - 2010