Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

Christopher Henson, Fabrizio Montesi [2026].
In CoRR abs/2602.15078.

Abstract

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.

Links

doi.org

Additional notes

None

Cite (BibTeX)

Click to expand

@article{DBLP:journals/corr/abs-2602-15078,
  author       = {Christopher Henson and
                  Fabrizio Montesi},
  title        = {Computer Science as Infrastructure: the Spine of the Lean Computer
                  Science Library (CSLib)},
  journal      = {CoRR},
  volume       = {abs/2602.15078},
  year         = {2026},
  url          = {https://doi.org/10.48550/arXiv.2602.15078},
  doi          = {10.48550/ARXIV.2602.15078},
  eprinttype   = {arXiv},
  eprint       = {2602.15078},
  timestamp    = {Sun, 29 Mar 2026 14:38:05 +0200},
  biburl       = {https://dblp.org/rec/journals/corr/abs-2602-15078.bib},
  bibsource    = {dblp computer science bibliography, https://dblp.org}
}

A PDF is available (possibly a preprint):

Some data from DBLP and Crossref.