cslib

Tech stack & purpose

CSLib is the Lean Computer Science Library, a formalisation of computer science theories and tools in Lean 4 that provides APIs for formal verification, certified software, and connecting different CS developments. Built with Lean 4 and Lake as its build system, it depends primarily on Mathlib. The library covers multiple problem domains including computability theory and automata, programming language formalisations (such as the Lambda Calculus and Calculus of Communicating Systems), logic formalisations (including Linear Logic and Hennessy-Milner Logic), cryptography, and distributed systems, with particular emphasis on semantics as a unifying foundation across these areas.

Community & reference links

• Lean prover Zulip chat
• Lean FRO radar instance

Languages

Contributors (top 30 of 48)

• 
  Fabrizio Montesi199 commits · 69 followers
• 
  Chris Henson98 commits · 42 followers
• 
  Kim Morrison46 commits · 552 followers
• 
  Ching-Tsun Chou36 commits · 14 followers
• 
  Eric Wieser18 commits · 532 followers
• 
  Garmelon15 commits · 42 followers
• 
  lyj15 commits · 85 followers
• 
  Jesse Alama12 commits · 133 followers
• 
  mathlib-nightly-testing[bot]11 commits · 0 followers
• 
  Thomas Krishna Waring11 commits · 8 followers
• 
  Maximiliano Onofre Martínez9 commits · 15 followers
• twwar9 commits
• 
  Samuel Schlesinger7 commits · 172 followers
• 
  Kenny Lau6 commits · 54 followers
• 
  euprunin6 commits · 0 followers
• 
  Felix Pernegger5 commits · 8 followers
• 
  Marcelo Lynch4 commits · 35 followers
• 
  WegmannDavid4 commits · 2 followers
• Tristan F.3 commits
• Alexandre Rademaker3 commits
• 
  Tanner Duve3 commits · 24 followers
• 
  Xueying Qin3 commits · 20 followers
• crei3 commits
• 
  Bolton Bailey3 commits · 58 followers
• 
  Iván Renison2 commits · 108 followers
• Juan Pablo Yamamoto2 commits
• Dhruv Gupta2 commits
• 
  Maximiliano Onofre Martínez2 commits · 15 followers
• Tristan F.-R.2 commits
• 
  Quang Dao1 commits · 104 followers