In two previous blog posts (part 1 and interlude), I presented a set of notions to prove asymptotic complexity of OCaml programs, then an OCaml implementation of Okasaki's "binary random access lists". In this last blog post, I combine the two ideas, and present a formalization of binary random access lists, using CFML.
This small interlude post is not about Coq nor CFML: I present a data structure from Okasaki's Purely functional data structures, implemented in OCaml.
It comes as a preliminary explanation for an incoming formalization of it in CFML (see next post), including an complexity analysis!
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 blog posts (current, interlude and final), 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.