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.

• Type: Conference
• Year: 2008
• Where: ESOP
• Authors: Rasmus Lerchedahl Petersen, Lars Birkedal, Aleksandar Nanevski, Greg Morrisett
• Keywords: Dependent Type Theory, ESOP 2008, Hoare Type Theory, Impredicative Hoare Type, Programming Languages