Programming Languages Delft

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."

dl.acm.org/doi/10.1145/3678000

#mucalculus #agda #effects #coinduction #tyde

timorl
Ugh, we are finishing up a paper for submission and one of my coauthors wanted to better understand the math that I produced and get more useful references for people unfamiliar with #coinduction. Unfortunately it seems that by grabbing two approaches that try to treat it as something natural and combining them I did something that no one else did before, so now every reference will be confusing, because it uses an at least slightly different approach...

How are we going to find reviewers for that. :blobfoxmeltsob:
Akkoma

social.wuatek.is