The Madness of the Modal mu-Calculus
Venue: MSP 101
Abstract: In this talk, I'll give you the "what", "why", and "how" of the μ-calculus - what it is, why I find it interesting (and hopefully why you should too!), and how to tame it in Agda. I'll start by introducing and motivating the field of model checking, before quickly diverting to the modal μ-calulus, a fixpoint modal logic of foundational importance in that field. I'll talk about its semantics first, because that's only sensible, then the rest of the talk will be devoted to the weird and wonderful (but mostly weird) syntactic issues that arise from this formalism. In particular, I'll focus on an important syntactic construction called "the closure" of a μ-calculus formula, which is not stable under alpha-equivalence, and whose inductive structure is somewhat non-obvious. In the second half, we'll code up an implementation of the μ-calculus in Agda, which will also serve as an introduction to well-scoped De Bruijn syntax. I'll work towards defining parallel substitution and weakening, and finish with the definition of the closure, and a (very) brief sketch of its correctness proof. The data type of thinnings between natural numbers will feature. If there's time (which there probably won't be), I'll discuss an extension of well-scoped De Bruijn syntax that I've been calling "sublimely-scoped" syntax, which is still very WIP.