In this talk we claim that various forms of "trace semantics" defined for concurrent systems with: different input/output types, or with different types of "concurrency" such as non-determinism or probability, are instances of a single categorical construction, namely coinduction in a Kleisli category. Hence we demonstrate the abstraction power of categorical--in particular coalgebraic--methods in computer science, which uncover basic mathematical structures underlying various concrete examples.

Our claim is based on our main technical result that an initial algebra in the category of sets and functions yields a final coalgebra in the Kleisli category, for monads with a suitable order structure. The proof relies on coincidence of limits and colimits, like in [Smyth & Plotkin, SIAM J. Comp.,1982].

The talk is meant to be self-contained, spending much time also for explaining basic preliminaries such as: traditional "trace semantics" coalgebraic modelling of concurrent systems monads, distributive laws, Kleili categories initial algebra via initial sequence, final coalgebra via final sequence limit-colimit coincidence by Smyth and Plotkin