| Summary: | 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.
|
|---|