基于交集类型的混合组合综合
摘要：合成使用类型栖息在交叉类型中的混合物的组合的方法。首先，利用记录的λ演算表示了递归定义的类和混合物。使用记录和记录合并的交叉类型给这些术语分配有意义的类型而不需要使用递归类型。其次，类型化的术语被转化为一个有类型组合子的仓库。我们展示了具有记录合并和构造函数的记录类型和交叉类型之间的关系。这个关系被用来证明翻译相对于混合物合成的声音性和部分完备性。此外，我们演示了如何将已翻译的仓库和目标类型作为输入用于通过类型栖息在有界组合逻辑中进行组合合成的现有框架。计算结果是一个由目标类型进行类型化并通过应用混合物合成到现有类而生成的类。
作者：Jan Bessai, Tzu-Chun Chen, Andrej Dudenhefner, Boris D"udder, Ugo de'Liguoro, Jakob Rehof
论文ID：1712.06906
分类：Logic in Computer Science
分类简称：cs.LO
提交时间：2023-06-22