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

TL;DR

This paper introduces CSLib, a centralized library for formalised computer science in Lean, detailing its foundational principles, semantic frameworks, automation tools, and initial language developments to support formal verification and software modeling.

Contribution

It presents the core design principles, semantic interfaces, automation support, and initial language models for CSLib, advancing formalised computer science in Lean.

Findings

Development of reusable semantic interfaces

Implementation of proof automation and CI/testing support

First substantial language and model developments

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.