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. © 2008 Springer-Verlag Berlin Heidelberg.
Cite
CITATION STYLE
Petersen, R. L., Birkedal, L., Nanevski, A., & Morrisett, G. (2008). A realizability model for impredicative Hoare Type Theory. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 4960 LNCS, pp. 337–352). https://doi.org/10.1007/978-3-540-78739-6_26
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
