Zulip Chat Archive

Stream: CSLib

Topic: Porting from rocq ?

Bas Spitters (Feb 08 2026 at 09:51):

Rocq has a huge CS library.
There are already some porting efforts under way (e.g. iris/stdpp) and softwarefoundations.cis.upenn.edu .
[ I also have some of my own that I'll announce separately. }

Did you consider porting, or at least taking inspiration from the Rocq eco-system?
The CS lib roadmap is not very detailed, so for now, I've just asked an LLM to do a quick comparison.
It's below (slightly edited). I'd be happy to help with a more detailed comparison.
The HOL eco-systems can also be a rich source for inspiration.

I believe this may also be a chance for deeper connections and collaboration between the eco-systems.
One such project we are working on is the peregrine-project.github.io. (for verified compilers, pilar II)

AI (mostly) generated

Here's a mapping of CSLib's three pillars to existing Rocq ecosystem projects that could serve as porting sources or inspiration:

Pillar 1: Formalizing CS Foundations

This is where the Rocq ecosystem is richest and most directly relevant.

Models of Computation (lambda calculus, Turing machines, computability)
- Formalised Undecidable Problems (coq-community) — This is the single most relevant library. It formalizes lambda calculus as a model of computation (Forster & Smolka's "L" calculus), Turing machines, Post correspondence problem, and a large web of reductions between undecidable problems. Built collaboratively by students at Saarland. Directly maps to CSLib's 6-month milestone.
- CoLoR — Library on rewriting theory, lambda-calculus and termination. Has sub-libraries on data structures extending the stdlib.
- Regular Language Representations — Translations between regular expressions, automata, etc. Covers formal language theory fundamentals.

Algorithms & Data Structures
- Functional Algorithms Verified in SSReflect (coq-community) — Verified implementations of searching, sorting, and other fundamental algorithms. Directly targets CSLib's "algorithms textbook" goal.
- Tarjan/Kosaraju SCC algorithms (coq-community) — Formalized graph algorithms with correctness proofs.
- Ceramist — Verified hash-based approximate membership structures (Bloom filters).
- CertiGraph — Library for reasoning about directed graphs and their embedding in separation logic.
- Graph Theory — Formalized graph theory results.

Randomized / Approximation Arguments
- FCF — Framework for proofs of cryptography (includes probabilistic reasoning).
- SSProve — Modular cryptographic proofs framework.

Logic & PL Foundations
- Coq Library for First-Order Logic — Syntax, semantics, and proof systems of FOL, built on the undecidability library. There was an active push to add this to the Rocq Platform.
- Completeness and Decidability of Modal Logic Calculi — Formalized K, K*, CTL, PDL. Relevant to CSLib's modal logic goals.
- Metalib — PL metatheory using locally nameless representations.
- Autosubst — Automated de Bruijn term handling, crucial infrastructure for PL formalization.

Math for CS (not in Mathlib)
- Rocq Stdlib itself has basic arithmetic, logic, data structures (lists, sets, maps), and decidability infrastructure.
- Coq-std++ (stdpp) — The extended alternative standard library used heavily by Iris. Has finite maps, finite sets, countable types, orders, etc. This is extremely well-engineered and would be a prime porting candidate for foundational data structures and reasoning infrastructure.
- Mathematical Components — While much overlaps with Lean's Mathlib, certain combinatorial and finite-type reasoning (fintypes, bigops) could fill CS-specific gaps.

Pillar 2: Reasoning about Code (Boole / imperative verification)

This is where Rocq's flagship projects live, but porting is harder because they're tightly integrated with Rocq-specific features.
Program Verification Tools
- Interaction Trees — Library for representing recursive and impure programs. Very relevant to Boole's need to handle effectful imperative code.
- FreeSpec — Modularly verifying programs with effects and effect handlers.
- Fiat — Automated synthesis of correct-by-construction programs.

Real-World Verification Projects (as case studies/inspiration)
- Verdi — Formally verified distributed systems.
- ConCert — Smart contract verification with extraction to contract languages. (included in https://peregrine-project.github.io/)
- Fiat-Crypto — Cryptographic primitive code generation (used in Chrome/BoringSSL).

Pillar 3: Repository of Verified Code

This is largely downstream of Pillars 1 and 2, but the Rocq ecosystem has relevant verified implementations:

Functional Algorithms Verified in SSReflect — Directly maps to the "algorithms textbook in Boole" goal.
Verified Functional Algorithms (Software Foundations Vol. 3) — Andrew Appel's textbook formalizations of data structures in Coq. A natural porting target.
Incremental Cycles — Verified OCaml implementation of incremental cycle detection.
CompCert programs verified via VST — There's a corpus of verified C programs. (also included in the https://peregrine-project.github.io/ pipeline)

The key insight is that Rocq has ~40 years of CS formalization that Lean largely lacks, and CSLib is explicitly trying to fill this gap. The Rocq community libraries are the most natural and license-compatible sources for porting foundational CS content.

Chris Henson (Feb 08 2026 at 10:20):

Small nitpick: I think it would be nice to move the wall of LLM text into a spoiler drop-down so the human text is easier to see in the flow of conversation.

I'll speak mostly on the lambda calculus formalizations I wrote. These modules, as noted in their docstrings, very directly take inspiration from Rocq and I wouldn't object to calling them a port. (The interesting deviations as I talked about in my Lean Together talk are how Lean's metaprogramming and grind change things). This isn't in CSLib yet, but I also spent a lot of time looking at Agda formalizations of lambda calculi because of how I believe their intrinsic typing judgements are needed for getting some version of categorical semantics in to Lean.

As I have mentioned previously, my next big project for CSLib is going to be very directly taking inspiration from Rocq and Nominal Isabelle in setting up metaprogramming utilities for declaring type systems and binding. Again the interesting part here is in synthesis of prior tooling of other proof assistants into something that looks a little bit different in Lean. In areas that I'm less familiar with, I know there have been discussions about making use of the recently added coinductive predicates, which would definitely closely reference prior work in Rocq.

There are several other examples I'll omit for brevity. So yes, it has not only been considered to take inspiration from Rocq and other proof assistants, but is already actively shaping the library. Several of the examples in the LLM generated text are things that I have already used as inspiration or will for future work. I would personally be welcoming of idiomatic (i.e. not fully AI translated) ports of developments from other proof assistants. The idiomatic piece here is crucial, especially when translating tactics and automation between proof assistants and using existing Mathlib abstractions.

Bas Spitters (Feb 08 2026 at 13:17):

Hi @Chris Henson I'll try to look up your talk later. Unfortunately, there are no slides here: https://leanprover-community.github.io/lt2026/schedule.html

From what you wrote, what you've done (looking at rocq and agda) is precisely what I tried to suggest.
I see you are a PhD-student. Have you considered how to get academic credit for your work, while also giving due credit to earlier formalizations?
I agree there are more idiomatic ways of translating then say Babel does (https://hal.science/hal-05342510/document)
But I'm also wondering how to justify porting of several hundreds of thousands of lines of code from Rocq to Lean, if we dont use assistance.

About nominal sets, our colleagues work on nominal SSProve is now in the main line: https://eprint.iacr.org/2025/598
Maybe it is of some use to you. I'd be interested in an idiomatic development in Lean.

Bas Spitters (Feb 08 2026 at 14:34):

This is classical POPLmark (reloaded) material. Someone (@Chris Henson ?) should do Lean4!
( or maybe it's already done, and then the websites would need to be updated...)

https://poplmark-reloaded.github.io/
https://www.seas.upenn.edu/~plclub/poplmark/

Chris Henson (Feb 08 2026 at 14:47):

Thanks for finding the links @Snir Broshi. To address your other questions @Bas Spitters :

Bas Spitters said:

Have you considered how to get academic credit for your work, while also giving due credit to earlier formalizations?

Yes, as I think is true of any PhD student publications are being considered! How to frame things is a question, but for instance the (very early) work I describe above regarding a Lean synthesis of Autosubst and related work is sufficiently novel in my view. Even the work in my talk linked above, while well trod in some sense, is interesting in seeing how it compares the first Rocq formalizations of locally nameless binding.

I agree there are more idiomatic ways of translating then say Babel does (https://hal.science/hal-05342510/document)
But I'm also wondering how to justify porting of several hundreds of thousands of lines of code from Rocq to Lean, if we dont use assistance.

Disclaimer: I am a single maintainer that does not speak unilaterally for CSLib and I'll be as brief as possible at the cost of nuance. My view is the many discussions you can find in other threads about "why do we formalize mathematics?" equally apply here. I'd ask a similar "why do we port to Lean?". For myself, I think it is because there is something inherently interesting to be found in discovering the "Lean way" of implementing the previous decades of PL research done in other proof assistants. For me, using AI to perform large ports does not align with my goals of careful exploring this space. The details are deceptively "simple"!

Bas Spitters said:

This is classical POPLmark (reloaded) material. Someone (Chris Henson ?) should do Lean4!
( or maybe it's already done, and then the websites would need to be updated...)

Yes, it is! I didn't include records, but the pure Fsub pieces (1A/2A) are complete, closely following Charguéraud. A new contributor is currently working on strong normalization for STLC.

Fabrizio Montesi (Feb 13 2026 at 12:22):

We take inspiration from projects (and papers) in other theorem provers, yes. Porting efforts or pointers to relevant projects are always welcome (just like any other formalisation effort in the scope of CSLib). Sometimes porting is not simple, as it requires a redesign to integrate well with CSLib and Mathlib (which we depend on).

Last updated: Feb 28 2026 at 14:05 UTC