Denotational World-indexed Logical Relations and Friends

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 fixed-point theorem for functors on certain metric spaces by America and Rutten. Also we investigate the use of recursively defined metric worlds in an operational setting and arrive at constructions akin to step-indexed models. On a different, 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 differently, 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 specific details about its module.