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.

Programming Languages Zoo

Systems language with linear types and capability-based security.

A statically-typed, functional typesetting system

Effects-based direct-style IO for multicore OCaml

OCaml - Oxidized!

Visual Studio Code extension for Coq

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

A Rust verification tool

Cooperative-threaded access to relational data

Modern scientific computing for OCaml

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.

OCaml graph library

😎TT

CoqHammer: An Automated Reasoning Hammer Tool for Rocq - Proof Automation for Dependent Type Theory

GUI library for ocaml based on SDL2

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

Hygienic typed literal macros (TLMs) for Reason

Prototype type inference engine

Visual Studio Code Extension and Language Server Protocol for Rocq / Coq

Higher-kinded programming in OCaml

Communication between Coq and SAT/SMT solvers