Parametrized Fixed Points on O-Categories and Applications to Session Types

TL;DR

This paper introduces a generalized functorial dagger operation for locally continuous functors on O-categories, satisfying Conway identities, with applications to session-typed language semantics.

Contribution

It extends existing techniques to define a functorial dagger on O-categories, satisfying Conway identities, and applies this to session-typed language semantics.

Findings

Dagger operation satisfies Conway identities.

Functorial dagger is defined on locally continuous functors.

Applications to session-typed language semantics.

Abstract

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.