(link to the article.) This is joint work with David Nowak, and Jean-Pierre Talpin.

Abstract

We define a categorical model of computation that mixes contextual and effectful computations, and give a compositional and executable semantics for stateful stream programs. We leverage the Yang-Baxter equation to define a new distributive law between certain monad and comonad. We use the Kleisli category of the resulting distributive law to define a semantics for a minimal yet powerful calculus of imperative stream processing functions. Along the way, we provide illustrative examples to clarify key concepts of the calculus and demonstrate the applicability of its formalization in a stateful implementation of the infinite sieve of Eratosthenes using the Rocq proof assistant.

References

[1]: Benjamin Lion, David Nowak, A Categorical Model of Computation for Stateful Stream Programming https://inria.hal.science/hal-05451358v1/document.

[2]: Benjamin Lion, Rocq implementation of the theory presented in the paper. n.d. “Bialgebraic semantics.” https://zenodo.org/records/17371682.