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 |
|---|---|
| Udgiver | |
| Status | Udgivet - 2010 |