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.

My research has always been supported by code or mechanized proofs: these are linked aside each corresponding paper in the publications page.

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..


I have contributed to the development of the OCaml compiler and smaller ocaml projects.

Check out pp_loc, a library that helps you produce user-friendly error messages by quoting the input fragment responsible for the error!