A Realizability Model for Impredicative Hoare Type Theory

DSpace/Manakin Repository

A Realizability Model for Impredicative Hoare Type Theory

Citable link to this page


Title: A Realizability Model for Impredicative Hoare Type Theory
Author: Petersen, Rasmus Lerchedahl; Birkedal, Lars; Nanevski, Aleksandar; Morrisett, John Gregory

Note: Order does not necessarily reflect citation order of authors.

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.
Access Status: Full text of the requested work is not available in DASH at this time (“dark deposit”). For more information on dark deposits, see our FAQ.
Full Text & Related Files:
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.
Published Version: doi:10.1007/978-3-540-78739-6_26
Other Sources: http://ynot.cs.harvard.edu/papers/HTTmodel.pdf
Citable link to this page: http://nrs.harvard.edu/urn-3:HUL.InstRepos:3980869
Downloads of this work:

Show full Dublin Core record

This item appears in the following Collection(s)


Search DASH

Advanced Search