文章基本信息

标题：Logical relations for coherence of effect subtyping
本地全文：下载
作者：Polesiuk, Piotr ; Biernacki, Dariusz
期刊名称：Logical Methods in Computer Science
印刷版ISSN：1860-5974
电子版ISSN：1860-5974
出版年度：2018
卷号：14
期号：1
语种：English
出版社：Technical University of Braunschweig
摘要：A coercion semantics of a programming language with subtyping is typicallydefined on typing derivations rather than on typing judgments. To avoidsemantic ambiguity, such a semantics is expected to be coherent, i.e.,independent of the typing derivation for a given typing judgment. In thisarticle we present heterogeneous, biorthogonal, step-indexed logical relationsfor establishing the coherence of coercion semantics of programming languageswith subtyping. To illustrate the effectiveness of the proof method, we developa proof of coherence of a type-directed, selective CPS translation from a typedcall-by-value lambda calculus with delimited continuations and control-effectsubtyping. The article is accompanied by a Coq formalization that relies on anovel shallow embedding of a logic for reasoning about step-indexing.