Search papers, labs, and topics across Lattice.
The paper introduces CSLib, a centralized library of formalized computer science and software built in the Lean theorem prover, analogous to Mathlib. It addresses the need for a shared, verified foundation for computer science knowledge, facilitating collaboration and reducing redundancy in formalization efforts. The authors present CSLib's technical principles, abstractions, semantic framework, and initial developments, including reusable semantic interfaces and proof automation.
Formalized computer science gets a Mathlib-inspired boost with CSLib, a new Lean library promising reusable semantics and automated proofs.
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.
