四个分隔控制操作符的类型系统
摘要：类型系统的控制运算符的操作行为在过去的几十年中已经进行了全面的研究，但是类型系统还没有涉及到控制运算符。存在着不同的转换系统用于shift,control,shift0，而且它们之间没有任何关系，也还没有与control0 直接对应的类型系统。本文通过给出一个统一的类型系统来解决这个问题，用于四个控制运算符。按照Danvy和Filinski的方法，我们从CPS解释器中推导出一个单态类型系统，该解释器定义了四个控制运算符的操作语义。通过在Agda中实现带类型的CPS解释器，我们展示了CPS翻译保持了类型，并且具有所有四个控制运算符的演算是终止的。此外，我们展示了我们的类型系统与之前的shift,control和shift0类型系统之间的关系。
作者：Chiaki Ishio and Kenichi Asai
论文ID：2305.02852
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-05-05