Imagen de Portada

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

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autores principales:	Henson, Christopher, Montesi, Fabrizio
Formato:	Preprint
Publicado:	2026
Materias:	Logic in Computer Science Programming Languages
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

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

CSLib: The Lean Computer Science Library
por: Barrett, Clark, et al.
Publicado: (2026)

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

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

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

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

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

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

Lean Meets Theoretical Computer Science: Scalable Synthesis of Theorem Proving Challenges in Formal-Informal Pairs
por: Zhang, Terry Jingchen, et al.
Publicado: (2025)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Algorithmically Expressive, Always-Terminating Model for Reversible Computation
por: Palazzo, Matteo, et al.
Publicado: (2024)

A Framework for Universality in Physics, Computer Science, and Beyond
por: Gonda, Tomáš, et al.
Publicado: (2023)

Proceedings 16th International Workshop on Graph Computation Models
por: Lambers, Leen, et al.
Publicado: (2026)

Proceedings of the Fourteenth and Fifteenth International Workshop on Graph Computation Models
por: Endrullis, Jörg, et al.
Publicado: (2025)

Towards a Characterization of Two-way Bijections in a Reversible Computational Model
por: Palazzo, Matteo, et al.
Publicado: (2025)

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

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

Recursive Mutexes in Separation Logic
por: Du, Ke, et al.
Publicado: (2026)

Outrunning Big KATs: Efficient Decision Procedures for Variants of GKAT
por: Zhang, Cheng, et al.
Publicado: (2026)

Symmetric Proofs of Parameterized Programs
por: Cheng, Ruotong, et al.
Publicado: (2026)

Can LLMs Perform Synthesis?
por: Egolf, Derek, et al.
Publicado: (2026)

Type Theory With Erasure
por: Theocharis, Constantine, et al.
Publicado: (2026)

A Program Logic for Abstract (Hyper)Properties
por: Baldan, Paolo, et al.
Publicado: (2026)

Ordered Adjoint Logic (Extended Version)
por: Roshal, Sophia, et al.
Publicado: (2026)

Bit-Vector CHC Solving for Binary Analysis and Binary Analysis for Bit-Vector CHC Solving
por: Bembenek, Aaron, et al.
Publicado: (2026)

TensorRocq: Enabling diagrammatic reasoning in Rocq
por: Caldwell, Benjamin, et al.
Publicado: (2026)