ITU

A Realizability Model for Impredicative Hoare Type Theory

Research output: Journal Article or Conference Article in JournalConference articleResearchpeer-review

View graph of relations

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
Book seriesLecture Notes in Computer Science
Pages (from-to)337-352
ISSN0302-9743
DOIs
Publication statusPublished - 2008
Event17th European Symposium on Programming, ESOP 2008 - Budapest, Hungary
Duration: 29 Mar 20086 Apr 2008
Conference number: 17

Conference

Conference17th European Symposium on Programming, ESOP 2008
Number17
CountryHungary
CityBudapest
Period29/03/200806/04/2008

ID: 265532