TY - RPRT
T1 - A Realizability Model for Impredicative Hoare Type Theory
AU - Lerchedahl Petersen, Rasmus
AU - Nanevski, Aleksandar
AU - Morrisett, Greg
AU - Birkedal, Lars
PY - 2007/9
Y1 - 2007/9
N2 - 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.
AB - 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.
M3 - Report
T3 - IT University Technical Report Series
BT - A Realizability Model for Impredicative Hoare Type Theory
PB - IT-Universitetet i København
CY - Copenhagen
ER -