Effectful Trace Semantics via Effectful Streams

Explore a 59-minute Topos Institute Colloquium presentation that delves into effectful streams as a coinductive semantic universe for effectful dataflow programming and traces. Learn how effectful streams are applied to formalize stream cipher cryptographic protocols and understand their particularization in monoidal categories with conditionals and ranges. Discover the development of trace and bisimulation concepts for effectful Mealy machines, and examine how bisimulation implies effectful trace equivalence. Based on collaborative research with Filippo Bonchi and Mario Román, gain insights into the mathematical foundations of effectful programming and semantic analysis.