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.
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.
Originalsprog | Engelsk |
---|---|
Bogserie | Lecture Notes in Computer Science |
Sider (fra-til) | 337-352 |
ISSN | 0302-9743 |
DOI | |
Status | Udgivet - 2008 |
Begivenhed | 17th European Symposium on Programming, ESOP 2008 - Budapest, Ungarn Varighed: 29 mar. 2008 → 6 apr. 2008 Konferencens nummer: 17 |
Konference
Konference | 17th European Symposium on Programming, ESOP 2008 |
---|---|
Nummer | 17 |
Land/Område | Ungarn |
By | Budapest |
Periode | 29/03/2008 → 06/04/2008 |
Emneord
- Denotational Model
- Impredicative Hoare Type Theory
- Dependent Type Theory
- Mutable Abstract Data Types
- Impredicative Polymorphism