论文标题
O类别和会话类型应用程序的参数化固定点
Parametrized Fixed Points on O-Categories and Applications to Session Types
论文作者
论文摘要
O类别将域类别概括为仅提供计算本地连续函数的固定点所需的结构。参数化的固定点特别感兴趣，对于“匕首操作”通常给出。我们概括了现有技术，以在O类别之间对本地连续函数定义函数匕首操作。我们表明，此匕首操作满足了Conway身份，这是用于迭代理论的一系列身份。我们研究了这种匕首操作对自然转化的行为，并考虑到针对会话类型语言的语义的应用。
O-categories generalize categories of domains to provide just the structure required to compute fixed points of locally continuous functors. Parametrized fixed points are of particular interest to denotational semantics and are often given by "dagger operations". We generalize existing techniques to define a functorial dagger operation on locally continuous functors between O-categories. We show that this dagger operation satisfies the Conway identities, a collection of identities used to axiomatize iteration theories. We study the behaviour of this dagger operation on natural transformations and consider applications to semantics of session-typed languages.
