## Abstract

As part of the long-standing drive for mathematical machinery to reason about

computer programs, we use the technique of denotational logical relations to prove

contextual equivalence of stateful programs. We propose the notion of approximate

locations to solve the non-trivial problem of existence and solve the fundamental

type-worlds circularity by metric-space theory. This approach scales to state-of-theart

step-indexed techniques and permits unrestricted relational reasoning by the use

of so-called Bohr relations.

Along the way, we develop auxiliary theory; most notably a generalized version

of a classical xed-point theorem for functors on certain metric spaces by America

and Rutten. Also we investigate the use of recursively dened metric worlds in an

operational setting and arrive at constructions akin to step-indexed models.

On a dierent, though related, note, we explore a relational reading of separation

logic with assertion variables. In particular, we give criteria for when standard,

unary separation logic proofs lift to the binary setting. Phrased dierently, given

a module-dependent client and a standard separation logic proof of its correctness,

we ponder the default question of representation-independence: is the client able to

{ or unable to { observe implementation specic details about its module.

computer programs, we use the technique of denotational logical relations to prove

contextual equivalence of stateful programs. We propose the notion of approximate

locations to solve the non-trivial problem of existence and solve the fundamental

type-worlds circularity by metric-space theory. This approach scales to state-of-theart

step-indexed techniques and permits unrestricted relational reasoning by the use

of so-called Bohr relations.

Along the way, we develop auxiliary theory; most notably a generalized version

of a classical xed-point theorem for functors on certain metric spaces by America

and Rutten. Also we investigate the use of recursively dened metric worlds in an

operational setting and arrive at constructions akin to step-indexed models.

On a dierent, though related, note, we explore a relational reading of separation

logic with assertion variables. In particular, we give criteria for when standard,

unary separation logic proofs lift to the binary setting. Phrased dierently, given

a module-dependent client and a standard separation logic proof of its correctness,

we ponder the default question of representation-independence: is the client able to

{ or unable to { observe implementation specic details about its module.

Originalsprog | Engelsk |
---|

Forlag | IT-Universitetet i København |
---|---|

Antal sider | 222 |

Status | Udgivet - 2010 |