2026-07-20T14:45:26Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:5158 2024-03-06T10:36:10Z ddc:004 open_access

Logical Relations for Coherence of Effect Subtyping Biernacki, Dariusz Polesiuk, Piotr type system coherence of subtyping logical relation control effect continuation-passing style 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dariusz Biernacki and Piotr Polesiuk 2015 Is Part Of LIPIcs, Volume 38, 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.TLCA.2015.107 urn:nbn:de:0030-drops-51580 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.TLCA.2015.107 eng https://creativecommons.org/licenses/by/3.0/legalcode