程序副词与Tl"on嵌入
摘要：自由单子（及其变体）已成为在证明助理中表示具有效果的程序语义的通用工具。这些数据结构支持通过未解释事件参数化的语义的组合定义，并且具有丰富的等式理论。但是，单子并不是结构有效计算的唯一方法，我们为什么要限制自己呢？ 在本文中，受适用函子，选择性函子和其他结构的启发，我们定义了一组数据结构和理论，称为程序修饰语，以捕获各种计算模式。程序修饰语本身是可组合的，允许它们用于指定具有多个计算模式的语言的语义。我们将程序修饰语作为一种新类别的语义嵌入的基础，称为Tl"on嵌入。与基于自由单子的嵌入相比，Tl"on嵌入在效果的计算建模中更灵活，同时保留了程序的语法结构的更多信息。
作者：Yao Li, Stephanie Weirich
论文ID：2207.05227
分类：Programming Languages
分类简称：cs.PL
提交时间：2022-07-28