Skip to content
Non-Rocq software
- ReGraph : Python library for building graph-based hierarchical knowledge representation systems. Russ Harmer & Eugenia Oshurko
- KAMI : Bio-curation tool to construct executable models of signalisation paths in Kappa. Russ Harmer & Eugenia Oshurko
- EmergeNS : Simulation of chemical reactions and detection of autocatalytic cycles. Denis Kuperberg
- Hypergraph : Online tool to edit and analyse hypergraphs and their treewidth. Damien Pous
- Click and Collect : An interactive linear logic prover. Olivier Laurent & Étienne Callies
- MLL Prover : Prototype of interactive prover with automatic context inference for MLL. Olivier Laurent & Jonas Torriero-Meskour
Tools and libraries for Rocq
- graph-theory : Library of formalised graph theory results. Damien Pous & Christian Doczkal
- relation-algebra : Library and automation tactics for binary relations. Damien Pous & Christian Doczkal
- coinduction : A library for doing proofs by (enhanced) coinduction. Damien Pous
- Yalla : Yet Another linear logic Library. Olivier Laurent
- approx-models : Library to verify rigorous approximations of univariate functions on real numbers. Damien Pous, Assia Mahboubi & Florent Bréhard
- OLlibs : Add-ons for the standard library. Olivier Laurent
- List Permutation : Canonical representation for permutations and their action on lists. Olivier Laurent & Christophe Lucas
- FormalizedLLBib : Collection of formalisations of linear logic. Olivier Laurent
Rocq formalisations
- Proof nets for MLL: Formalisation of multiplicative proof nets. Olivier Laurent & Rémi Di Guardia
- Quantifiers : Formalisation of the “anti-locally nameless” approach to quantifiers. Olivier Laurent
- RieszRocq : Formalization for the article “Free modal Riesz spaces are Archimedean: a syntactic proof”. Matteo Mio & Christophe Lucas
