A Realizability Model for Impredicative Hoare Type Theory

Rasmus Lerchedahl Petersen, Aleksandar Nanevski, Greg Morrisett, Lars Birkedal

Research output: Book / Anthology / Report / Ph.D. thesisReportResearch

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.
Original languageEnglish
Place of PublicationCopenhagen
PublisherIT-Universitetet i København
EditionTR-2007-101
Number of pages31
Publication statusPublished - Sept 2007
Externally publishedYes
SeriesIT University Technical Report Series
NumberTR-2007-101
ISSN1600-6100

Fingerprint

Dive into the research topics of 'A Realizability Model for Impredicative Hoare Type Theory'. Together they form a unique fingerprint.

Cite this