José A. Alonso
Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. https://arxiv.org/abs/2602.15078v1 #LeanProver #ITP #CSLib #CompSci
Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
Following in the footsteps of the success of Mathlib - the centralised library of formalised mathematics in Lean - CSLib is a rapidly-growing centralised library of formalised computer science and software. In this paper, we present its founding technical principles, operation, abstractions, and semantic framework. We contribute reusable semantic interfaces (reduction and labelled transition systems), proof automation, CI/testing support for maintaining automation and compatibility with Mathlib, and the first substantial developments of languages and models.
Hennessy-Milner logic in CSLib, the Lean computer science library. ~ Fabrizio Montesi, Marco Peressotti, Alexandre Rademaker. https://arxiv.org/abs/2602.15409v1 #LeanProver #ITP #CSLib #CompSci
Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
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.
ACP SectionRE: https://mastodon.acm.org/@acp/115921453909423834
The recording for @fmontesi's Lean Together talk, "CSLib: The Lean Computer Science Library", is now online:
@fmontesi is presenting the first results and next steps of CSLib – the Lean Computer Science library – at Lean Together tomorrow (20 Jan) at 14:00 CET. The event is online and open to all, so feel free to join if you're curious:
Fabrizio Montesi ⬣ A➔BFORM (https://sdu.dk/form) is a new research centre at the University of Southern Denmark. It is a major investment in formalised computer science and reliable AI-assisted programming. We collaborate heavily with the #Lean FRO and other international partners on #CSLib.
~ Academic Positions in Formal Methods (postdoc, assistant prof., associate prof.) and Programming Languages (postdoc) ~
The first positions at the Centre for Formal Methods and Future Computing (FORM, https://www.sdu.dk/form) are here! Among other projects, FORM is also working on the formalisation of computer science as part of a global initiative, CSLib, in @leanprover.
(1/3)
#formalMethods #LeanProver #typeTheory #programmingLanguages #academicJobs #fediHire #FORMSDU #SDUDK #CSLib
@fmontesi will be the first director of the new Centre for Formal Methods and Future Computing (FORM) here at the University of Southern Denmark!
Among other things, the Centre will work on the development of @leanprover's CS Library, where Fabrizio already serves as a member of the steering committee.
Interested in research in formal methods? Please expect job announcements very soon.
#formalMethods #LeanProver #CSLib #programmingLanguages #FORMSDU #SDUDK