Rational Codata as Syntax-with-Binding: Correct-by-Construction Foundations of the Modal µ-Calculus

extended abstract

Abstract: We present a work-in-progress formalisation of Kozen's result that the Fischer-Ladner closure for any formula of the modal -calculus is finite. Our proof hinges on the rational nature of the closure, exploiting a technique first demonstrated by Ghani et al. for representing rational codata types inductively as syntax-with-binding.