A Realizability Model for Impredicative Hoare Type Theory

Rasmus Lerchedal Petersen; Lars Birkedal; Alexandar Nanevski; Greg Morrisett

doi:10.1007/978-3-540-78739-6_26

A Realizability Model for Impredicative Hoare Type Theory

Rasmus Lerchedal Petersen, Lars Birkedal, Alexandar Nanevski, Greg Morrisett

Research output: Journal Article or Conference Article in Journal › Conference article › Research › peer-review

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.

Original language	English
Book series	Lecture Notes in Computer Science
Pages (from-to)	337-352
ISSN	0302-9743
DOIs	https://doi.org/10.1007/978-3-540-78739-6_26
Publication status	Published - 2008
Event	17th European Symposium on Programming, ESOP 2008 - Budapest, Hungary Duration: 29 Mar 2008 → 6 Apr 2008 Conference number: 17

Conference

Conference	17th European Symposium on Programming, ESOP 2008
Number	17
Country/Territory	Hungary
City	Budapest
Period	29/03/2008 → 06/04/2008

Keywords

Denotational Model
Impredicative Hoare Type Theory
Dependent Type Theory
Mutable Abstract Data Types
Impredicative Polymorphism

Access to Document

10.1007/978-3-540-78739-6_26

Cite this

@inproceedings{bc9670f08fc811dd8006000ea68e967b,

title = "A Realizability Model for Impredicative Hoare Type Theory",

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.",

keywords = "Denotational Model, Impredicative Hoare Type Theory, Dependent Type Theory, Mutable Abstract Data Types, Impredicative Polymorphism, Denotational Model, Impredicative Hoare Type Theory, Dependent Type Theory, Mutable Abstract Data Types, Impredicative Polymorphism",

author = "Petersen, {Rasmus Lerchedal} and Lars Birkedal and Alexandar Nanevski and Greg Morrisett",

note = "Serie: Lecture Notes in Computer Science, Springer, 4960, 0302-9743, 1611-3349 Volumne: 4960/2008; 17th European Symposium on Programming, ESOP 2008 ; Conference date: 29-03-2008 Through 06-04-2008",

year = "2008",

doi = "10.1007/978-3-540-78739-6_26",

language = "English",

pages = "337--352",

journal = "Lecture Notes in Computer Science",

issn = "0302-9743",

publisher = "Springer",

}

TY - GEN

T1 - A Realizability Model for Impredicative Hoare Type Theory

AU - Petersen, Rasmus Lerchedal

AU - Birkedal, Lars

AU - Nanevski, Alexandar

AU - Morrisett, Greg

N1 - Conference code: 17

PY - 2008

Y1 - 2008

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.

KW - Denotational Model

KW - Impredicative Hoare Type Theory

KW - Dependent Type Theory

KW - Mutable Abstract Data Types

KW - Impredicative Polymorphism

KW - Denotational Model

KW - Impredicative Hoare Type Theory

KW - Dependent Type Theory

KW - Mutable Abstract Data Types

KW - Impredicative Polymorphism

U2 - 10.1007/978-3-540-78739-6_26

DO - 10.1007/978-3-540-78739-6_26

M3 - Conference article

SN - 0302-9743

SP - 337

EP - 352

JO - Lecture Notes in Computer Science

JF - Lecture Notes in Computer Science

T2 - 17th European Symposium on Programming, ESOP 2008

Y2 - 29 March 2008 through 6 April 2008

ER -