Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker

TL;DR
This paper formalizes Hennessy-Milner Logic within the Lean CSLib library, providing syntax, semantics, and a complete proof of the Hennessy-Milner theorem, emphasizing generality, reusability, and automation.
Contribution
It introduces a parametric, reusable formalization of HML in CSLib, including the full metatheory and integration with Lean's automation tools.
Findings
Complete formalization of HML in CSLib
Proof of Hennessy-Milner theorem for image-finite LTSs
Reusable library code available for systems using CSLib
Abstract
We present a library-level formalisation of Hennessy-Milner Logic (HML) - a foundational logic for labelled transition systems (LTSs) - for the Lean Computer Science Library (CSLib). Our development includes the syntax, satisfaction relation, and denotational semantics of HML, as well as a complete metatheory including the Hennessy-Milner theorem - bisimilarity coincides with theory equivalence for image-finite LTSs. Our development emphasises generality and reusability: it is parametric over arbitrary LTSs, definitions integrate with CSLib's infrastructure (such as the formalisation of bisimilarity), and proofs leverage Lean's automation (notably the grind tactic). All code is publicly available in CSLib and can be readily applied to systems that use its LTS API.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsLogic, programming, and type systems · Model-Driven Software Engineering Techniques · Semantic Web and Ontologies
