效应子类型相干性的逻辑关系
Logical relations for coherence of effect subtyping
AI总结：
本文提出异质、双正交、步进索引的逻辑关系，用于证明带子类型编程语言强制语义的相干性，并以带限定续延和效应子类型的CPS变换为例验证，附有Coq形式化。
摘要：
具有子类型关系的编程语言的强制语义通常定义在类型推导上，而非类型判断上。为避免语义歧义，此类语义需具备相干性，即对于给定的类型判断，其语义应与类型推导无关。本文提出异质、双正交、步进索引的逻辑关系，用于建立具有子类型关系的编程语言强制语义的相干性。为展示该证明方法的有效性，我们针对带限定续延和控制效应子类型的类型化按值调用lambda演算，开发了类型导向的选择性CPS变换的相干性证明。本文附有Coq形式化，其依赖于一种新颖的浅嵌入逻辑，用于推理步进索引。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
