xavierleroy
Professor of software sciences at Collège de France, Paris. Member of Inria research team Cambium. Interested in all scientific aspects of computer programming
Collège de France and InriaParis, France
Pinned Repositories
CompCert
The CompCert formally-verified C compiler
ocaml
The core OCaml system: compilers, runtime system, base libraries
camlidl
Stub code generator for OCaml/C interface
camlzip
Reading and writing zip and gzip files from OCaml
cdf-mech-sem
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
cdf-program-logics
Companion Coq development for Xavier Leroy's 2021 lectures on program logics
coq2html
An HTML documentation generator for Coq source files
cryptokit
A library of cryptographic primitives (ciphers, hashes, etc) for OCaml
ocamlmpi
OCaml/MPI interface
pringo
A library of splittable pseudo-random number generators for OCaml
xavierleroy's Repositories
xavierleroy/cryptokit
A library of cryptographic primitives (ciphers, hashes, etc) for OCaml
xavierleroy/cdf-mech-sem
Coq development for the course "Mechanized semantics", Collège de France, 2019-2020
xavierleroy/camlzip
Reading and writing zip and gzip files from OCaml
xavierleroy/cdf-program-logics
Companion Coq development for Xavier Leroy's 2021 lectures on program logics
xavierleroy/pringo
A library of splittable pseudo-random number generators for OCaml
xavierleroy/camlidl
Stub code generator for OCaml/C interface
xavierleroy/coq2html
An HTML documentation generator for Coq source files
xavierleroy/ocamlmpi
OCaml/MPI interface
xavierleroy/ocamlagrep
String searching with errors, using the Wu-Manber algorithm
xavierleroy/cdf-sem-meca
Développement Coq pour le cours "Sémantiques mécanisées", Collège de France, 2019-2020
xavierleroy/canonical-binary-tries
Coq development accompanying the paper "Efficient Extensional Binary Tries"
xavierleroy/spamoracle
E-mail filter and classifier based on Bayesian learning
xavierleroy/camljava
Low-level OCaml/Java interface
xavierleroy/ocaml
The core OCaml system: compilers, runtime system, base libraries
xavierleroy/ocamltopwin
Historical Win32 application for the OCaml toplevel
xavierleroy/arm64-barriers
Performance issues with ARM64 barriers
xavierleroy/experimental
Experiments with Git and Github
xavierleroy/graphics
The Graphics library from OCaml, in a standalone repository
xavierleroy/opam-coq-archive
Archive for all Coq related OPAM packages organized in various repositories
xavierleroy/opam-repository
Main public package repository for OPAM, the source package manager of OCaml.
xavierleroy/coq
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.
xavierleroy/coq-mmaps
Modular Finite Maps overs Ordered Types
xavierleroy/ocaml-multicore
Multicore OCaml
xavierleroy/ocaml.org
The official OCaml website.
xavierleroy/RFCs
Design discussions about the OCaml language
xavierleroy/sandmark
Fork of Sandmark, A benchmark suite for the OCaml compiler
xavierleroy/Zarith
The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.