José A. Alonso @Jose_A_Alonso@mathstodon.xyz
Public

Computer science as infrastructure: the spine of the Lean computer science library (CSLib). ~ Christopher Henson, Fabrizio Montesi. arxiv.org/abs/2602.15078v1

arXiv logo

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

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.

arxiv.org · arXiv.org

0
0
0

If you have a fediverse account, you can quote this note from your own instance. Search https://mathstodon.xyz/users/Jose_A_Alonso/statuses/116096680427641916 on your instance and quote it. (Note that quoting is not supported in Mastodon.)