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.

翻译：继Mathlib——精益（Lean）中形式化数学的集中式库——的成功之后，CSLib是一个快速发展的、集中式的形式化计算机科学与软件库。本文阐述了其基础技术原理、运行机制、抽象体系及语义框架。我们贡献了可复用的语义接口（归约与标记转移系统）、证明自动化、用于维护自动化及与Mathlib兼容性的持续集成/测试支持，以及首批语言与模型的实质性开发成果。