vbgl Vincent Laporte
github.com/vbgl · maintains 464 packages (463 directly), sole maintainer of 388, member of 0 teams
464 packages · page 5 of 5
| Package ▼ | Version | Maintainers | # | Teams | Deps | Used by | Used by (transitive) | Status |
|---|---|---|---|---|---|---|---|---|
Simple cross-platform OCaml code editor built for top-level evaluation |
1.2.0 |
1 | 7 | 0 | 0 | single | ||
Convert a filesystem into a static OCaml module |
4.1.0 |
1 | 7 | 9 | 13 | single | ||
Simple tool which produces pretty-printed output from a Menhir parser file (.mly) |
0.8.1 → 0.91 |
1 | 7 | 0 | 0 | single outdated | ||
SAT solver binary based on the msat library |
0.9.1 |
1 | 8 | 0 | 0 | single | ||
Modular and Open Platform for Static Analysis using Abstract Interpretation |
1.1 → 1.2 |
1 | 17 | 0 | 0 | single outdated | ||
Performance monitoring and benchmarking suite |
5.5.2 |
1 | 3 | 0 | 0 | single | ||
C runtime libraries of ANTLR v3 |
3.4 → 3.5.3 |
1 | 2 | 2 | 27 | single outdated | ||
Workbench for high-assurance and high-speed cryptography |
2026.09.0 |
1 | 16 | 0 | 0 | single | ||
Interactive theorem prover based on Higher-Order Logic |
0-unstable-2026-09-02 → 20231021 |
3 | 12 | 0 | 0 | maintained outdated | ||
Reference implementation of the Dirfile Standards |
0.11.0 |
1 | 4 | 0 | 0 | single | ||
Verifying and formally proving properties on numerical programs dealing with floating-point or fixed-point arithmetic |
1.8.0 → 1.8.3 |
1 | 8 | 0 | 0 | single outdated | ||
XMPP chat client |
2.6.0 |
4 | 52 | 0 | 0 | maintained | ||
Testing program for EasyCrypt formalizations |
2026.09 |
1 | 11 | 0 | 0 | single | ||
Computer-Aided Cryptographic Proofs |
2026.09 |
1 | 16 | 0 | 0 | single | ||
Composable build system |
2.9.3 |
1 | 5 | 0 | 0 | single | ||
Composable build system |
3.23.1 → 3.24.2 |
1 | 5 | 1,215 | 1,402 | single outdated | ||
High-performance theorem prover and SMT solver |
1.8 |
2 | 15 | 3 | 22 | maintained | ||
Command line tool for handling CSV files |
2.4 |
1 | 7 | 0 | 0 | single | ||
Coq proof assistant |
9.3.0 |
4 | 10 | 0 | 0 | maintained | ||
Coq proof assistant |
9.2.0 |
4 | 10 | 1 | 1 | maintained | ||
Coq proof assistant |
9.0.1 |
4 | 7 | 0 | 0 | maintained | ||
Coq proof assistant |
8.9.1 |
4 | 5 | 0 | 0 | maintained | ||
Coq proof assistant |
8.8.2 |
4 | 5 | 0 | 0 | maintained | ||
Coq proof assistant |
8.7.2 |
4 | 5 | 0 | 0 | maintained | ||
Coq proof assistant |
8.20.1 |
4 | 5 | 1 | 8 | maintained | ||
Coq proof assistant |
8.19.2 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.18.0 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.17.1 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.16.1 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.15.2 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.14.1 |
4 | 6 | 0 | 0 | maintained | ||
Coq proof assistant |
8.13.2 |
4 | 9 | 0 | 0 | maintained | ||
Coq proof assistant |
8.12.2 |
4 | 9 | 0 | 0 | maintained | ||
Coq proof assistant |
8.11.2 |
4 | 9 | 0 | 0 | maintained | ||
Coq proof assistant |
8.10.2 |
4 | 9 | 0 | 0 | maintained | ||
Extended “Standard Library” for Rocq |
1.13.0 |
2 | 5 | 2 | 2 | maintained | ||
2.5.0 |
3 | 8 | 5 | 10 | maintained | |||
Purely functional IO for Coq |
1.11.0 |
1 | 6 | 1 | 2 | single | ||
Yet Another Coq Library on Machine Words |
3.5 |
1 | 9 | 2 | 2 | single | ||
2.5.0 |
3 | 7 | 1 | 13 | maintained | |||
2.5.0 |
3 | 7 | 2 | 32 | maintained | |||
2.5.0 |
3 | 7 | 9 | 29 | maintained | |||
2.5.0 |
3 | 7 | 5 | 12 | maintained | |||
2.5.0 |
3 | 7 | 2 | 2 | maintained | |||
2.5.0 |
3 | 6 | 17 | 44 | maintained | |||
2.5.0 |
3 | 8 | 11 | 26 | maintained | |||
2.5.0 |
3 | 7 | 0 | 0 | maintained | |||
Jasmin language & verified compiler |
2026.03.3 |
2 | 7 | 0 | 0 | maintained | ||
Rocq development of the Iris Project |
4.5.0 |
2 | 5 | 0 | 0 | maintained | ||
Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant |
4.11.5 |
1 | 11 | 3 | 3 | single | ||
Finite data structures with extensional reasoning |
0.5.0 |
1 | 6 | 1 | 1 | single | ||
Build dependency graphs between Coq objects |
1.0+9.1 |
1 | 4 | 0 | 0 | single | ||
Generic instances of MathComp classes |
0.2.3 |
1 | 6 | 2 | 2 | single | ||
Coq library for Reals |
3.4.5 |
1 | 7 | 2 | 4 | single | ||
Library to certify primality using Pocklington certificate and Elliptic Curve Certificate |
8.20 |
1 | 5 | 0 | 0 | single | ||
Reconstruction tactics for the hammer for Coq |
1.3.3+9.1 |
1 | 5 | 1 | 1 | single | ||
General-purpose automated reasoning hammer tool for Coq |
1.3.3+9.1 |
1 | 5 | 0 | 0 | single | ||
Formally verified C compiler |
3.18 |
3 | 9 | 3 | 3 | maintained unfree | ||
Coq proof assistant |
9.1.1 |
4 | 7 | 78 | 85 | maintained | ||
Formally verified C compiler |
3.18 |
3 | 11 | 0 | 0 | maintained unfree | ||
Open-source linear programming solver written in C++ |
1.17.11 |
1 | 6 | 9 | 68 | single | ||
Powerful editor targeted towards programmers and webdevelopers |
2.4.2 |
1 | 10 | 0 | 0 | single | ||
Classical Arabic typeface in Naskh style |
1.003 |
1 | 2 | 0 | 0 | single | ||
Font for Arabic-based writing systems in the Kano region of Nigeria and in Niger |
3.000 |
1 | 3 | 0 | 0 | single |