Elena Di Lavore: 'Effectful trace semantics via effectful streams'

Topos Institute Colloquium, 16th of May 2024.
———
Effectful streams are a coinductive semantic universe for effectful dataflow programming and traces. As an example, we formalise the stream cipher cryptographic protocol. In monoidal categories with conditionals and ranges, effectful streams particularize to families of morphisms satisfying a causality condition. Effectful streams allow us to develop notions of trace and bisimulation for effectful Mealy machines; bisimulation implies effectful trace equivalence.

This is recent joint work with Filippo Bonchi and Mario Román.