Parametrized Fixed Points on O-Categories and Applications to Session Types
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.
Cite
@article{arxiv.2006.08479,
title = {Parametrized Fixed Points on O-Categories and Applications to Session Types},
author = {Ryan Kavanagh},
journal= {arXiv preprint arXiv:2006.08479},
year = {2020}
}
Comments
Accepted at the 36th International Conference on Mathematical Foundations of Programming Semantics --- MFPS 2020