Armaël Guéneau

I enjoy programming, both for fun and to support my research.
Currently, most of the coding happens on my github account or the logsem organization.

Coq libraries

cfml-bigO: an extension of the CFML framework with support for verifying the complexity of programs with big-O bounds. Some of it has now been integrated in CFML itself (for instance the support for negative time credits).

procrastination: a small library for collecting side conditions and deferring their proof. This is also part of the methodology that I developed during my PhD for carrying out complexity proofs.

minicooper: a formally verified implementation of Cooper's quantifier elimination procedure, as a Coq reflexive tactic.

Formally verified software

During my PhD, I worked on formalizing not only the functional correctness of algorithms, but also their asymptotic complexity.

BRAL (code, proof): a simple Binary Random Access List (purely functional) data structure, providing list and array operations with O(log n) amortized cost.

incremental-cycles: implementation and proof of a state-of-the-art algorithm (published in 2015!) for incremental cycle detection. The OCaml implementation is provided as a reusable library, and is already used in production, as part of the Dune build system for ocaml. The implementation of the Coq kernel also uses a more advanced version of this algorithm for checking universe constraints, and its (good) complexity is critical for performance. The goal is to ultimately replace it with formally verified code, once we extend our proof to the version of the algorithm used in Coq.

OCaml

I contribute to the development of the OCaml compiler, for which I have the "maintainer" hat.

I enjoy engaging and collaborating with other members of the ocaml community. Across the years I have contributed both small and larger amounts of code to a number of ocaml projects (including opam, ocaml-mustache, dmlenu, ...), and I am also the author of a few libraries and tools.

Marracheck

Marracheck is an ongoing experimentation in collaboration with Gabriel Scherer, as an attempt to build (yet another) tool that can build all packages in the opam repository for ocaml while doing a minimal amount of work (for CI purposes).

In particular, we have experimented with custom solver backends for opam to efficiently solve "best effort" queries with a large number of packages. We also insisted in reusing the opam libraries as much as possible, which made us in turn contribute improvements back to opam itself. (See our rough design notes, in French.)

Note that more production ready tools exist with the same use case (with a different design and tradeoffs): Kate's opam-health-check, Damien Doligez and Florian Angeletti's opamcheck and ocamllabs' ocurrent ci.