Logical relations for coherence of effect subtyping

TL;DR

This paper introduces a novel logical relation framework to prove the coherence of coercion semantics in programming languages with subtyping, demonstrated through a formal proof in Coq for a complex language translation.

Contribution

It presents heterogeneous, biorthogonal, step-indexed logical relations for coherence proofs, with a formal Coq implementation for a language with advanced features.

Findings

Proves coherence of coercion semantics for subtyping in programming languages.

Develops a formal Coq proof for a complex language translation.

Introduces a novel shallow embedding for reasoning about step-indexing.

Abstract

A coercion semantics of a programming language with subtyping is typically defined on typing derivations rather than on typing judgments. To avoid semantic ambiguity, such a semantics is expected to be coherent, i.e., independent of the typing derivation for a given typing judgment. In this article we present heterogeneous, biorthogonal, step-indexed logical relations for establishing the coherence of coercion semantics of programming languages with subtyping. To illustrate the effectiveness of the proof method, we develop a proof of coherence of a type-directed, selective CPS translation from a typed call-by-value lambda calculus with delimited continuations and control-effect subtyping. The article is accompanied by a Coq formalization that relies on a novel shallow embedding of a logic for reasoning about step-indexing.