English

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

Category Theory 2020-06-16 v1 Programming Languages

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.

Keywords

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

R2 v1 2026-06-23T16:20:24.316Z