Stars
A static analyzer for Java, C, C++, and Objective-C
The Rocq Prover is an interactive theorem prover, or proof assistant. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environmen…
Programming language for literate programming law specification
Implementations of various type systems in OCaml.
Systems language with linear types and capability-based security.
A statically-typed, functional typesetting system
Effects-based direct-style IO for multicore OCaml
The Ott tool for writing definitions of programming languages and calculi
QuickCheck inspired property-based testing for OCaml.
Proof assistant based on the λΠ-calculus modulo rewriting
Cooperative-threaded access to relational data
Lock-free data structures for multicore OCaml
The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.
CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory
A proof assistant for higher-dimensional type theory
Type-checker for the λΠ-calculus modulo rewriting
"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory
Visual Studio Code Extension and Language Server Protocol for Rocq / Coq [maintainers=@gbdrt,@SkySkimmer,@tabareau]