Modal Mu-Calculus for Free in Agda
summary
Embeds the modal μ-calculus into Agda by representing possibly nonterminating effectful programs as a coinductive free monad encoded with coinductive records and containers to ensure strict positivity. Delivers a runnable encoding (ATM example) that checks reachability, liveness and a parametric safety property, proves metatheory for a Hennessy‑Milner fragment, and exposes the full implementation and ongoing work on complete semantics and concurrency on GitHub.
AI-written summary · about
chapters (13)
- 0:00Verifying cyber-physical systems
- 1:28What is modal mu-calculus
- 3:35Complex properties with mu-calc
- 6:04Problem with model verification
- 6:45Why use coinductive free monad
- 8:54Free monad for programs
- 9:35ATM example in Agda
- 10:20Expressing properties
- 12:47Limitations and future work
- 14:36Resources and implementation
- 15:19Q&A: Comparison with transition systems
- 16:46Q&A: Extracting program behavior
- 18:54Q&A: Satisfaction relation
related talks
12mA Unified View of Modalities in Type Systems
17mMu tilde (re)cycled
26mTemporal refinements for Call-By-Push-Value with fixpoint
27mThe Relative Monadic Metalanguage
25mFormalizing pi-Calculus in Guarded Cubical Agda
20mFully Abstract Models for Effectful λ-Calculi via Category-Theoretic Logica
18mA modal deconstruction of Löb induction
14mModal Effect Types