These are public posts tagged with #coinduction. You can interact with them if you have an account anywhere in the fediverse.
Paper by Ivan Todorov and Casper Bach Poulsen at TyDe '24: Modal μ-Calculus for Free in Agda
"Using dependently-typed programming in Agda, we develop an embedding of the modal μ-calculus for defining and verifying functional properties of possibly-non-terminating effectful programs which we represent in Agda using the coinductive free monad."