Dariusz Biernacki ; Piotr Polesiuk - Logical relations for coherence of effect subtyping

lmcs:4180 - Logical Methods in Computer Science, January 30, 2018, Volume 14, Issue 1 - https://doi.org/10.23638/LMCS-14(1:11)2018
Logical relations for coherence of effect subtypingArticle

Authors: Dariusz Biernacki ; Piotr Polesiuk

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.

https://doi.org/10.23638/LMCS-14(1:11)2018
Source: arXiv.org:1710.09469
Volume: Volume 14, Issue 1
Secondary volumes: Selected Papers of the 26th International Conference on Rewriting Techniques and Applications and the 13th International Conference on Typed Lambda Calculus and Applications (RTA and TLCA 2015)
Published on: January 30, 2018
Accepted on: January 5, 2018
Submitted on: January 4, 2018
Keywords: Computer Science - Programming Languages
Licence: arXiv.org - Non-exclusive license to distribute

2 Documents citing this article

Share and export

Consultation statistics

This page has been seen 3376 times.
This article's PDF has been downloaded 1242 times.