Cover Image

CSLib: The Lean Computer Science Library

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Barrett, Clark, Chaudhuri, Swarat, Montesi, Fabrizio, Grundy, Jim, Kohli, Pushmeet, de Moura, Leonardo, Rademaker, Alexandre, Yingchareonthawornchai, Sorrachai
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Hennessy-Milner Logic in CSLib, the Lean Computer Science Library
by: Montesi, Fabrizio, et al.
Published: (2026)

Computer Science as Infrastructure: the Spine of the Lean Computer Science Library (CSLib)
by: Henson, Christopher, et al.
Published: (2026)

ProofWala: A Framework for Multilingual Proof Data Synthesis and Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2025)

An In-Context Learning Agent for Formal Theorem-Proving
by: Thakur, Amitayush, et al.
Published: (2023)

CSLibPremiseBench: Structure-Guided Premise Retrieval and Label Robustness for Lean 4 Computer-Science Theorems
by: Ji, Junye
Published: (2026)

Small Scale Reflection for the Working Lean User
by: Gladshtein, Vladimir, et al.
Published: (2024)

Proceedings Twentieth International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice
by: Chaudhuri, Kaustuv, et al.
Published: (2025)

Proceedings Twelfth Workshop on Fixed Points in Computer Science
by: Saurin, Alexis
Published: (2025)

PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition
by: Tsoukalas, George, et al.
Published: (2024)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

Learning Quantitative Automata Modulo Theories
by: Hsiung, Eric, et al.
Published: (2024)

Lean-auto: An Interface between Lean 4 and Automated Theorem Provers
by: Qian, Yicheng, et al.
Published: (2025)

CLEVER: A Curated Benchmark for Formally Verified Code Generation
by: Thakur, Amitayush, et al.
Published: (2025)

Probabilistic unifying relations for modelling epistemic and aleatoric uncertainty: semantics and automated reasoning with theorem proving
by: Ye, Kangfeng, et al.
Published: (2023)

Relational Hoare Logic for Realistically Modelled Machine Code
by: Mazzucato, Denis, et al.
Published: (2025)

Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects
by: Zilberstein, Noam, et al.
Published: (2023)

Canonicity for Cost-Aware Logical Framework via Synthetic Tait Computability
by: Li, Runming, et al.
Published: (2025)

Automating Bitvector and Finite Field Equivalence Proofs in Lean
by: Pertseva, Elizaveta, et al.
Published: (2026)

A Coq Library of Sets for Teaching Denotational Semantics
by: Cao, Qinxiang, et al.
Published: (2024)

Reasoning about Interior Mutability in Rust using Library-Defined Capabilities
by: Poli, Federico, et al.
Published: (2024)

Verifying an Effect-Handler-Based Define-By-Run Reverse-Mode AD Library
by: de Vilhena, Paulo Emílio, et al.
Published: (2021)

The termination of Nielsen transformations applied to word equations with length constraints
by: Przybocki, Benjamin, et al.
Published: (2025)

On Propositional Dynamic Logic and Concurrency
by: Acclavio, Matteo, et al.
Published: (2024)

Formulas as Processes, Deadlock-Freedom as Choreographies (Extended Version)
by: Acclavio, Matteo, et al.
Published: (2025)

Lean-SMT: An SMT tactic for discharging proof goals in Lean
by: Mohamed, Abdalrhman, et al.
Published: (2025)

String Diagrams for $λ$-calculi and Functional Computation
by: Ghica, Dan, et al.
Published: (2023)

Reversible Computation with Stacks and "Reversible Management of Failures"
by: Palazzo, Matteo, et al.
Published: (2025)

Semantic Properties of Computations Defined by Elementary Inference Systems
by: Lucas, Salvador
Published: (2025)

Exploiting the Potential of Linearity in Automatic Differentiation and Computational Cryptography
by: Giusti, Giulia
Published: (2025)

MerLean-Prover: A Recursive Looping Harness for Lean 4 Theorem Proving
by: Li, Jinzheng, et al.
Published: (2026)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages
by: Carette, TItouan, et al.
Published: (2022)

Proceedings 13th International Workshop on Developments in Computational Models
by: Alves, Sandra, et al.
Published: (2024)

RapunSL: Untangling Quantum Computing with Separation, Linear Combination and Mixing
by: Matsushita, Yusuke, et al.
Published: (2025)

Qunity: A Unified Language for Quantum and Classical Computing (Extended Version)
by: Voichick, Finn, et al.
Published: (2022)

Nazrin: Atomic Tactics for Graph Neural Networks for Theorem Proving in Lean 4
by: Aniva, Leni, et al.
Published: (2026)

A Probabilistic Choreography Language for PRISM
by: Carbone, Marco, et al.
Published: (2025)

Internalizing Representation Independence with Univalence
by: Angiuli, Carlo, et al.
Published: (2020)