Publication: A Realizability Model for Impredicative Hoare Type Theory
Date
2008
Published Version
Journal Title
Journal ISSN
Volume Title
Publisher
Springer Verlag
The Harvard community has made this article openly available. Please share how this access benefits you.
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.
Research Data
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.
Description
Other Available Sources
Keywords
Terms of Use
Metadata Only