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

Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive develo…

Tidy, feature-complete Web framework

Implementations of various type systems in OCaml.

A language server for reason, in reason

Functional language for parallel programming

Examples to illustrate the use of algebraic effects in Multicore OCaml

Declarative terminal graphics for OCaml

Links: Linking Theory to Practice for the Web

Documentation compiler for OCaml and Reason

A proof assistant for general type theories

1ML prototype interpreter

Lock-free data structures for multicore OCaml

Coq to Rust program extraction. The whole tree is on the original Coq code base.

😎TT

"Between the darkness and the dawn, a red cube rises!": a proof assistant for cartesian cubical type theory

Prototype type inference engine

A correct C89/C90/C99/C11/C18 parser written using Menhir and OCaml

A garden of small programming language implementations 🪴

drom is a wrapper over opam/dune in an attempt to provide a cargo-like user experience. It can be used to create full OCaml projects with sphinx and odoc documentation. It has specific knowledge of…

Parallel Programming over Domains

A proof assistant for higher-dimensional type theory

Visual Studio Code Extension and Language Server Protocol for Coq

Staged metaprogramming in stock OCaml

typed bidirectional router for OCaml/ReasonML web applications

Coq plugin embedding elpi

Simple template for midsize OCaml project

The essence of Rust.

Normalization by Evaluation for Martin-Löf Type Theory

Streamlining the release of dune packages to opam