Fabrizio Montesi - CSLib: The Lean Computer Science Library

Stream: Lean Together 2026

[Markus Himmel]

Discussion thread for the talk.

[Fabrizio Montesi]

Thanks for all the great questions! Lovely to see interest in CSLib.

[Syed Shaazib Tanvir]

Is there some place where we can follow the development of Boole? The cslib repository seems to only have a placeholder README in Cslib/Languages/Boole/ right now.

[Chris Henson]

If anyone was wanting to look closer at the code samples Fabrizio shared, our docs are hosted at https://api.cslib.io/docs/

[Fabrizio Montesi]

Syed Shaazib Tanvir said:

Is there some place where we can follow the development of Boole? The cslib repository seems to only have a placeholder README in Cslib/Languages/Boole/ right now.

There's a boole-sandbox branch: https://github.com/leanprover/cslib/tree/Boole-sandbox/Cslib/Languages/Boole

But bear in mind that the language design is still under discussion, things might (probably will) change. But it should give a general idea. The directory is still not very organised yet.

[Chris Henson]

You can also look directly at Strata, the dependency that gives access to Boole.

[Markus de Medeiros]

Would all formalizations of deeply embedded languages be required to use Boole/Strata? Or is the plan to have a framework for eg. operational semantics, and have the Boole/Strata languages instantiate it?

[Chris Henson]

(the branch Fabrizio mentioned pins a particular revision of Strata for its usage of Boole)

[Fabrizio Montesi]

Markus de Medeiros said:

Would all formalizations of deeply embedded languages be required to use Boole/Strata? Or is the plan to have a framework for eg. operational semantics, and have the Boole/Strata languages instantiate it?

It's still under discussion, and sometimes tricky because of some peer dependency issues. I expect the Lean module system to help with some of this at least though.

We do have a framework for operational semantics in CSLib, and some languages that instantiate it already (also in CSLib, like lambda and CCS). That's the framework we're building a downstream compiler on.

[Fabrizio Montesi]

All of automata theory is built on the operational semantics framework, too.

[Markus de Medeiros]

Ah very good, thank you! We were considering formalizing the languages framework for Iris-Lean, but maybe we should try using the CSLib formalization instead :)

[Chris Henson]

Also note that if you are considering lambda calculi as a deeply embedded language, these are independent of Boole and I imagine will remain so. I will talk tomorrow briefly of the future work I have planned for unifying our treatment of lambda calculi.

[Ching-Tsun Chou]

Are the slides of @Fabrizio Montesi 's presentation available somewhere? It was too early in the morning for me to attend.

[Fabrizio Montesi]

As soon as my website's CI/CD pipeline finishes... ;-)

Edit: it's done.

[Fabrizio Montesi]

Slides: https://www.fabriziomontesi.com/files/slides/cslib-lean-together-2026.pdf

[Shreyas Srinivas]

Is there are recording of the talk available somewhere?

[Ching-Tsun Chou]

#Lean Together 2026 > Key information @ 💬