The core OCaml system: compilers, runtime system, base libraries

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…

opam is a source-based package manager. It supports multiple simultaneous compiler installations, flexible package constraints, and a Git-friendly development workflow.

OCaml Language Server Protocol implementation

Source code of the Coccinelle project (mirror of the main Coccinelle repository located at Inria)

A lightweight, modular standard library extension, string library, and interfaces to various libraries (unix, threads, etc.) BSD license.

QuickCheck inspired property-based testing for OCaml.

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

Quick C-- compiler (no longer maintained)

An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, cl…

A CI for OCaml projects

Algorithms Implemented in OCaml

Python bindings for the Coq interactive proof assistant

Linear Dependent Types for Differential Privacy TypeChecker

An interactive tool for experimenting with LR(1) grammars

Example Coq plugin

DualQuery: Practical Private Query Release Algorithm

A compiler for the Algol W programming language.

Compiler for a variant of the "IMP" programming language

Source code for the blog series Writing a Lisp.

Just another Programming Language (JPL) interpreter / [todo: compiler]

A design for a systems programming language in the Pascal family.