Sciweavers

Share
ESOP
2008
Springer

A Realizability Model for Impredicative Hoare Type Theory

9 years 1 months ago
A Realizability Model for Impredicative Hoare Type Theory
We present a denotational model of impredicative Hoare Type Theory, a very expressive dependent type theory in which one can 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.
Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksan
Added 19 Oct 2010
Updated 19 Oct 2010
Type Conference
Year 2008
Where ESOP
Authors Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
Comments (0)
books