Rational codata as syntax-with-binding : correct-by-construction foundations of the modal μ-calculus

Tools

Watters, Sean (2025) Rational codata as syntax-with-binding : correct-by-construction foundations of the modal μ-calculus. In: 31st Conference on Types for Proofs and Programs, 2025-06-09 - 2025-06-13, University of Strathclyde.

[thumbnail of Watters-TYPES-2025-Rational-codata-as-syntax-with-binding]
Preview
 Text. Filename: Watters-TYPES-2025-Rational-codata-as-syntax-with-binding.pdf
Final Published Version
License: Strathprints license 1.0
Download (133kB)| Preview

Abstract

The modal µ-calculus is an extension of the basic modal logic K with least and greatest fixpoint operators. It is of foundational importance in the field of model checking, and also of considerable theoretical interest to logicians for its rich properties. The model checking and satisfiability problems for the µ-calculus are decidable, yet the logic is highly expressive — it subsumes the temporal logics LTL, CTL, CTL* and propositional dynamic logic, and is equivalent to the bisimulation-invariant fragment of monadic second-order logic. Of interest to the practising type theorist, the µ-calculus admits a constructive semantics in containers which is currently in the early stages of being explored. This (still work-in-progress) project is concerned with formalising the correctness and finiteness proofs for a particular key syntactic construction on µ-calculus formulas, namely their (Fischer-Ladner) closure. This can be thought of as a succinct graph representation of the formula. The definition of the closure is not structurally recursive, and indeed, the proof of its finiteness (originally due to Kozen) is fairly technical, particularly in a formal setting where issues like variable binding and substitution must be treated seriously. A key feature of our work is the use of syntax-with-binding as an inductive presentation of rational codata — data structures that loop back on themselves — in a manner similar to the technique first demonstrated by Ghani et al, and Hamana. We work in Agda, using guarded corecursion. At the time of submission, the bulk of the formalisation is complete (up to and including Theorem 1). Theorem 2 is still a work-in-progress.

ORCID iDs

Watters, Sean ORCID logoORCID: https://orcid.org/0009-0007-1249-254X;
CORE (COnnecting REpositories)