LFCS Seminars: 11 June 2019 - Sergey Goncharov

Title: Towards Coherence for Guarded Traces

Abstract:

Abstract guardedness is a unifying mechanism allowing for the identification of the equational theory of partial trace operators in (symmetric) monoidal categories in a compositional way. Examples include classical total iteration and recursion, partial recursion in categories of pre-domains and complete metric spaces, partial iteration in categories for modeling concurent processes and hybrid programs, as well as traces in infinite-dimensional Hilbert spaces. A salient feature of guarded traces is that they can be thought of both in a structural and in a geometric way. A precise connection between these two complementing views amounts to formulating and proving a suitable coherence theorem, which appears to be strikingly more subtle to state than its unguarded analogue. I present recent approached towards establishing such a coherence result. This is a joint work (in progress) with Lutz Schröder and Paul Levy.