A Realizability Model for Impredicative Hoare Type Theory

Petersen, Rasmus Lerchedahl; Birkedal, Lars; Nanevski, Aleksandar; Morrisett, John Gregory

View/Open

Petersen_Realizability.pdf (279.0Kb)

Access Status

Full text of the requested work is not available in DASH at this time ("restricted access"). For more information on restricted deposits, see our FAQ.

Author

Petersen, Rasmus Lerchedahl

Birkedal, Lars

Nanevski, Aleksandar

Morrisett, John Gregory HARVARD

Published Version

https://doi.org/10.1007/978-3-540-78739-6_26

Metadata

Show full item record

Citation

Petersen, Rasmus L., Lars Birkedal, Aleksandar Nanevski, and Greg Morrisett. 2008. A realizability model for impredicative Hoare Type Theory. In Programming Languages and Systems, ed. S. Drossopoulou, 337-352. Berlin; New York: Springer. Previously published in Lecture Notes in Computer Science 4960: 337-352.

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.