一句话：构造 distributor 诱导的双范畴模型，为 λ-演算提供交类型系统的 proof-relevant 语义并刻画可解性。
本文研究由 distributor 诱导的一族 λ-演算双范畴模型，并证明它们可由交类型系统进行语法呈现。作者首先引入一类 2-单子，其代数是用于刻画资源管理的 monoidal 范畴；随后将该单子提升到 distributor 上，定义参数化 Kleisli 双范畴，并给出其笛卡尔闭性的充分条件。在此框架中，作者定义 proof-relevant 语义：项的语义对应于其在相应类型系统中的类型推导集合。通过将可归约性（reducibility）技术适配到该设定，作者证明该模型能够刻画 λ-项的可解性。最后，文章描述了两个构造实例。
We study a family of distributors-induced bicategorical models of λ-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.