交类型分配子

我们研究一类由分配子诱导的 λ-演算双范畴模型，证明它们可通过交类型系统进行语法呈现。我们首先引入一类 2-单子，其代数为建模资源管理的幺半范畴。我们将这些单子提升到分配子上并定义参数化 Kleisli 双范畴，给出其笛卡尔闭的充分条件。在此框架中我们定义一种证明相关语义：项的解读将其在适当系统中的类型推导集合与之关联。我们证明我们的模型刻画可解性，将可归约性技术适配到我们的设定中。最后我们描述该构造的两个例子。