OCaml

ocaml-vdomLexiFi/ocaml-vdom

OCaml bindings for browser DOM APIs and an implementation of the Elm architecture with virtual DOM for building web applications.

GeoCoqGeoCoq/GeoCoq

A formalization of geometry in Coq based on Tarski's axiom system, containing both foundational and high-school style proofs.

Coq LSPejgallego/coq-lsp

A language server and VS Code extension providing incremental checking, error recovery, and IDE features for the Rocq/Coq proof assistant.

dromOCamlPro/drom

A wrapper over opam/dune providing a cargo-like experience for creating and managing OCaml projects with integrated documentation and CI.

Verdi Raftuwplse/verdi-raft

A formally verified implementation of the Raft distributed consensus protocol in Coq using the Verdi framework.

Coq-ElpiLPCIC/coq-elpi

A Coq plugin that embeds the Elpi λProlog interpreter to define new commands and tactics for theorem proving.

gen_js_apiLexiFi/gen_js_api

A tool for generating OCaml bindings to JavaScript libraries, simplifying cross-language interoperability.

TyreDrup/tyre

A typed regular expression library for OCaml that enables type-safe parsing and unparsing with automatic group extraction.

pfffreturntocorp/pfff

An OCaml API for static analysis, dynamic analysis, code visualization, navigation, and style-preserving source-to-source transformations.

OSnapeWert-Online/osnap

A high-performance snapshot testing tool focused on speed and ease of use, built with OCaml.

Redexerplum-umd/redexer

A binary instrumentation framework for analyzing and modifying Android app Dalvik bytecode.

libadalangAdaCore/libadalang

A library for parsing and semantic analysis of Ada code, designed as a building block for IDE integration and static analysis tools.

ppx_deriving_yojsonwhitequark/ppx_deriving_yojson

A ppx_deriving plugin that generates JSON serializers and deserializers for OCaml types using the Yojson library.

lablqmlKakadu/lablqml

A library for creating QtQuick/QML GUI applications in OCaml and Reason, providing bindings and a PPX syntax extension.

Fiatmit-plv/fiat

A Coq library for deductive synthesis of correct-by-construction abstract data types and parsers.

Caqti setence preparation, ppx_rapperroddyyaga/ppx_rapper

A syntax extension for writing type-safe SQL queries in OCaml with named parameters and PostgreSQL syntax checking.

OMicroBstevenvar/omicrob

A generic OCaml virtual machine for running OCaml programs on resource-constrained microcontrollers like AVR and PIC32.

Opalpyrocat101/opal

A minimal, self-contained library of monadic parser combinators for OCaml, enabling easy construction of recursive-descent parsers.

Spookyftripier/spookyc

A compiler for the Spooky programming language, designed to be the scariest language with spooky emoji keywords and unpredictable runtime behavior.

Markup.mlaantron/markup.ml

Error-recovering streaming HTML5 and XML parsers for OCaml with lazy, non-blocking, and one-pass processing.

routesanuragsoni/routes

A typed bidirectional router for OCaml and ReasonML web applications, enabling type-safe route definitions and URL generation.

SPOCmathiasbourgoin/SPOC

A PPX-based DSL for writing GPU kernels in OCaml syntax that compiles to multiple backends (CUDA, OpenCL, Vulkan, Metal).

jingootategakibunko/jingoo

An OCaml template engine with near-complete compatibility with Jinja2 syntax and features.

Miourobur-coop/miou

A simple, rule-based scheduler for OCaml 5 enabling concurrent and parallel task development with a focus on composability.

SerAPIejgallego/coq-serapi

A library for machine-to-machine interaction with the Coq proof assistant, providing serialization of Coq's internal datatypes to JSON or S-expressions.

Formalised Undecidable Problemsuds-psl/coq-library-undecidability

A Coq library containing mechanized reductions to establish undecidability results for problems in logic and computation.

SQLite3mmottl/sqlite3-ocaml

OCaml bindings to the SQLite3 database client API, enabling database operations from OCaml applications.

Sequoiaandrenth/sequoia

A type-safe query builder for OCaml that enforces SQL correctness at compile time using the OCaml type system.

pgxarenadotio/pgx

A pure OCaml PostgreSQL client library with support for Async, LWT, and synchronous operations.

ocaml-parsingsmolkaj/ocaml-parsing

A library and skeleton for writing OCaml parsers with beautiful error messages and minimal boilerplate.

Camomileyoriyuki/Camomile

A comprehensive Unicode library for OCaml providing character handling, string encodings, collation, and locale-sensitive operations.

biocamlbiocaml/biocaml

A high-performance, user-friendly OCaml library for bioinformatics applications.

Omlrleonid/oml

A comprehensive OCaml library for mathematical and statistical analysis with descriptive, typed APIs.

omlhammerlab/oml

A comprehensive OCaml library for mathematical and statistical analysis with typed, descriptive APIs.

WasmCert-CoqWasmCert/WasmCert-Coq

A mechanized formalization of WebAssembly 2.0 in Coq (Rocq) with soundness proofs and an extracted interpreter.

Decompressmirage/decompress

A pure OCaml library implementing DEFLATE, Zlib, Gzip, and LZO compression/decompression algorithms.