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…

Universal toplevel for OCaml

Auto-formatter for OCaml code

A Game Boy emulator written in OCaml that runs in your browser 🐫 🎮

A garden of small programming language implementations 🪴

A proof assistant for higher-dimensional type theory

OCaml bindings for raylib and raygui

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

Assemble dune workspaces to build your project and its dependencies as a whole

Build dependency graphs between Coq objects [maintainers=@Karmaki,@ybertot]

A dependent type theory with user defined data types

A simple, lightweight library for ANSI styling.

A functional programming language with polymorphic algebraic effects, handlers, and signature restriction