效应子类型的一致性的逻辑关系
摘要：具有子类型的编程语言的强制语义通常是在类型推导上定义的，而不是在类型判断上定义的。为了避免语义的不明确性，这样的语义被期望是一致的，即在给定的类型判断上独立于类型推导。在本文中，我们提出了异构、双正交、步进索引逻辑关系来建立具有子类型的编程语言强制语义的一致性。为了说明证明方法的有效性，我们开发了一个对类型导向的、选择性的CPS转换的一致性证明，从一个具有被限制续延和控制效应子类型的类型化的按值调用的lambda演算开始。该文章附带了一个基于一种用于推理步进索引的逻辑的新型浅嵌入的Coq形式化。
作者：Dariusz Biernacki and Piotr Polesiuk
论文ID：1710.09469
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22