Xavier Leroy's Projects
Stub code generator for OCaml/C interface
Low-level OCaml/Java interface
Reading and writing zip and gzip files from OCaml
Coq development accompanying the paper "Efficient Extensional Binary Tries"
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
Companion Coq development for Xavier Leroy's 2021 lectures on program logics
Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
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 development of machine-checked proofs.
Modular Finite Maps overs Ordered Types
An HTML documentation generator for Coq source files
A library of cryptographic primitives (ciphers, hashes, etc) for OCaml
Experiments with Git and Github
The Graphics library from OCaml, in a standalone repository
The core OCaml system: compilers, runtime system, base libraries
Multicore OCaml
Implementation of the ocaml.org website.
String searching with errors, using the Wu-Manber algorithm
OCaml/MPI interface
Historical Win32 application for the OCaml toplevel
Archive for all Coq related OPAM packages organized in various repositories
Main public package repository for OPAM, the source package manager of OCaml.
A library of splittable pseudo-random number generators for OCaml
Design discussions about the OCaml language
Fork of Sandmark, A benchmark suite for the OCaml compiler
E-mail filter and classifier based on Bayesian learning
The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.