Logical Relations for Coherence of Effect Subtyping

Authors Dariusz Biernacki, Piotr Polesiuk

Thumbnail PDF


  • Filesize: 0.49 MB
  • 16 pages

Document Identifiers

Author Details

Dariusz Biernacki
Piotr Polesiuk

Cite AsGet BibTex

Dariusz Biernacki and Piotr Polesiuk. Logical Relations for Coherence of Effect Subtyping. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 107-122, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)


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.
  • type system
  • coherence of subtyping
  • logical relation
  • control effect
  • continuation-passing style


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads