Papers With

← All papers
First page of Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)

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

Christopher Henson, Fabrizio Montesi

cs.LO Feb 16, 2026 · v1
tooling verification mathlib
Read PDF arXiv abstract
TL;DR
Presents CSLib, a centralized Lean library of formalized computer science with Mathlib-compatible automation.
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.
Problem

Lean has Mathlib for mathematics, but there is no analogous centralized library for formalized computer science and software in Lean.

Approach

CSLib (Computer Science Library) provides shared abstractions (reduction systems, labelled transition systems), proof automation as a first-class design constraint, CI/testing support for maintaining automation compatibility with Mathlib, and reusable semantic interfaces. The library reuses Mathlib infrastructure wherever possible and offers typeclass-based operational semantics frameworks.

Results

CSLib is a rapidly growing library that has enabled major formalization developments in computer science. It maintains compatibility with Mathlib and provides general-purpose proof automation for CS-specific reasoning patterns.