论文标题
相交类型的分销商
Intersection Type Distributors
论文作者
论文摘要
我们研究了分销商诱导的lambda-calculus的生物模型的家族，证明它们可以通过相交类型系统句法呈现。我们首先介绍了一类2个月填充的类，其代数是对资源管理进行建模的单体类别。我们将这些单子提升为分销商，并定义一个参数kleisli bicategory，为其笛卡尔封闭提供了足够的条件。在此框架中，我们定义了与证据相关的语义：与其在适当系统中的键入派生集的术语解释。我们证明了我们的模型表征可解决性，并将可降低性技术调整到我们的设置中。我们通过描述了两个构建的例子来结束。
We study a family of distributors-induced bicategorical models of lambda-calculus, proving that they can be syntactically presented via intersection type systems. We first introduce a class of 2-monads whose algebras are monoidal categories modelling resource management. We lift these monads to distributors and define a parametric Kleisli bicategory, giving a sufficient condition for its cartesian closure. In this framework we define a proof-relevant semantics: the interpretation of a term associates to it the set of its typing derivations in appropriate systems. We prove that our model characterize solvability, adapting reducibility techniques to our setting. We conclude by describing two examples of our construction.
