A Realizability Model for Impredicative Hoare Type Theory

Rasmus Lerchedal Petersen, Lars Birkedal, Alexandar Nanevski, Greg Morrisett

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftKonferenceartikelForskningpeer review

    Abstract

    We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can specify and reason about mutable abstract data types.
    The model ensures soundness of the extension of Hoare Type Theory with impredicative polymorphism; makes the connections to separation logic clear, and provides a basis for investigation of further sound extensions of the theory, in particular equations between computations and types.
    OriginalsprogEngelsk
    BogserieLecture Notes in Computer Science
    Sider (fra-til)337-352
    ISSN0302-9743
    DOI
    StatusUdgivet - 2008
    Begivenhed17th European Symposium on Programming, ESOP 2008 - Budapest, Ungarn
    Varighed: 29 mar. 20086 apr. 2008
    Konferencens nummer: 17

    Konference

    Konference17th European Symposium on Programming, ESOP 2008
    Nummer17
    Land/OmrådeUngarn
    ByBudapest
    Periode29/03/200806/04/2008

    Emneord

    • Denotational Model
    • Impredicative Hoare Type Theory
    • Dependent Type Theory
    • Mutable Abstract Data Types
    • Impredicative Polymorphism

    Citationsformater