In a recent paper, Arthur Charguéraud and François Pottier present a formal proof of an OCaml implementation of Tarjan's union-find algorithm. The proof covers two aspects: first, functional correctness ("the algorithm is correct"), but also asymptotic complexity. For example, one of the results of the paper is that the
link function runs in \(O(α(n))\) elementary steps, \(α\) being the inverse of the Ackermann function.
Actually, the complexity results of the paper are not presented using the "big-O" notation, commonly used in asymptotic complexity proofs: the various constants are explicit and manipulated through the proof.
In these two blog posts, I'll describe a tentative extension of CFML, the Coq library François and Arthur used for their proof. Its goal is to enable asymptotic reasoning, big-O notations and such to be used to prove complexity of programs.
Coq offers several internal evaluation mechanisms that have many uses, from glorious proofs by reflection to mundane testing of functions. Read on for an account of my quest to get large parts of the CompCert verified C compiler to execute from within Coq. It was a mighty battle between the forces of transparency and opacity, with the innocent-looking "decide equality" tactic as the surprise villain...
This is the second post on the Gagallium participation to the ICFP programming context last year -- 2014. See the first post for the introduction and a link to the source code; this post details the design of the ghost code.
The dates for the 2015 ICFP programming contest have been announced on the contest webpage. This is a good occasion to dig out a summary of our 2014 participation, that had been written over the span of several months (mostly right after the contest), and that we had unexplainably failed to publish before.
In 2013, some Gallium members (Thibaut Balabonski, Thomas Braibant, Jacques-Henri Jourdan and Gabriel Scherer) participated to the ICFP programming contest, and it was a lot of fun. We participated again in 2014, with a bit less gallium in the team (blame the precarity of post-docs, and some badly-chosen dates for a honeymoon) and a skewed alphabetic distribution: François Bobot, Pierre Boutillier, Thomas Braibant, Damien Doligez and Gabriel Scherer.
This (double) blog post was written over the course of the last ~5 months by three different persons. With hindsigth, we could probably have phrased some of the post differently. We believe that this blog post is best enjoyed as a pot-pourri of our thoughts, much like our ragtag submission.
At the very end of 2011, and then at the very beginning of 2013, I worked for some weeks on namespaces for OCaml (what they could be, why would we need them, what would be a good solution). The resulting proposal was too complex to gather steam, so I moved on -- and never got around to making the documents publicly available. Here they are.
How and why I designed my own approximated implementations
cos. The approximation error is quite
small, and the functions are fast and vectorizable. For example, my
logapprox function is 7.5x faster in tight loops than
function, while being more precise.
Contrary to top-down (LL) parsers, which do not support left recursion, bottom-up (LR) parsers support both left recursion and right recursion. When defining a list-like construct, a user of an LR parser generator, such as Menhir, faces a choice between these two flavors. Which one should she prefer?
Two considerations guide this choice: expressiveness (which flavor leads to fewer conflicts?) and performance (which flavor leads to a more efficient parser?).
In this post, I am mainly interested in discussing expressiveness. I also comment on performance in the setting of Menhir.
As we will see, the bottom line is that neither formulation seems deeply preferable to the other.
I share with Pierre Dagand the pleasure of having finished the redaction of a small article on realizability for JFLA 15 (Journées francophones des langages applicatifs). It is a rather simple presentation of the computational content of adequacy proofs, which we hoped to understand better by exhibiting their proof terms as well-typed lambda-terms in a dependently typed meta-language.
I just finished the proof of a property of the simply-typed lambda-calculus that hopefully can serve as a termination argument to decide whether a type has a unique inhabitant.
The 10-pages note containing the proof is available, and all comments are warmly welcome -- in particular about an already-existing proof of this result, I don't know about any. The rest of this post is (a HeVeA rendering of) the introduction, motivating the problem and presenting the fact to be proved -- or disproved. Feel free to ask yourself whether it is true or false before looking at the full note. The answer is at the last sentence of the introduction (only in the note).
It is interesting that we don't have much intuition about whether the result is true or false -- I changed my mind several times about it, and people asked about it guessed different way. The proof, however, is relatively simple and not particularly technically involved -- but I spent a few days simplifying the concepts and the notations.
We have just submitted the final version of two papers, presenting the state of our recent research.
- A Formally-Verified C Static Analyzer, by Jacques-Henri Jourdan, Vincent Laporte, Sandrine Blazy, Xavier Leroy, and David Pichardie
- Verified compilation of floating-point computations, by Sylvie Boldo, Jacques-Henri Jourdan, Xavier Leroy, and Guillaume Melquiond