Fabrizio Montesi ⬣ A➔BThanks to all for a great meeting. It's been energising, and I'm looking forward to the next interactions.
#CSLib #AI #Lean #FORM #FormalMethods
3/3
If you're not on the Lean Community Zulip, you can get the Zoom link to join the meeting here. I'll post it in a comment to this post when the time comes.
#Lean #FormalMethods #CSLib #FORM
2/2
We offer a library-level solution in #CSLib through the 'HasFresh' typeclass. Whatever the type of x is, you just need to convince #Lean that there's a 'fresh' value generator and you're good to go with your proofs. For many types (like natural numbers), we've even already convinced Lean for you.
This way, you can make reusable definitions that work for any type x might have, instead of hardcoding your model on something ad hoc.
2/
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:
FORM (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