Parametrized Fixed Points and Their Applications To Session Types
Parametrized Fixed Points and Their Applications To Session Types
Electronic Notes in Theoretical Computer Science
352
October 2020
The 36th Mathematical Foundations of Programming Semantics Conference, 2020
149-172
10.1016/j.entcs.2020.09.008
Parametrized fixed points are of particular interest to denotational semantics and are often given by “dagger operations”. Dagger operations that satisfy the Conway identities are particularly useful, because these identities imply a large class of identities used in semantic reasoning. We generalize existing techniques to define dagger operations on $$\omega$$-categories and on $$\textbf{O}$$-categories. These operations enjoy a 2-categorical structure that implies the Conway identities. We illustrate these operators by considering applications to the semantics of session-typed languages.