文章基本信息

标题：Logical Relations for Coherence of Effect Subtyping
本地全文：下载
作者：Dariusz Biernacki ; Piotr Polesiuk
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2015
卷号：38
页码：107-122
DOI：10.4230/LIPIcs.TLCA.2015.107
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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