A blog at Gallium: informal posts about research, programming practice, OCaml development, and general ramblings.

## Formally verifying the complexity of OCaml programs with CFML -- part 3

- August 3, 2015

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.

## Formally verifying the complexity of OCaml programs with CFML -- interlude

- July 30, 2015
- Last updated on 2015/08/03

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!

## Formally verifying the complexity of OCaml programs with CFML -- part 1

- July 18, 2015
- Last updated on 2015/08/03

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.

## Using Coq's evaluation mechanisms in anger

- June 23, 2015

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

## ICFP programming contest 2014: a retrospective (part 2/2)

- May 25, 2015
- Last updated on 2015/05/25

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.

## ICFP programming contest 2014: a retrospective (part 1/2)

- May 22, 2015

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.

## Namespace archeology

- March 19, 2015

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.

## Fast vectorizable math functions approximations

- January 26, 2015
- Last updated on 2015/01/27

How and why I designed my own approximated implementations
of `log`

, `exp`

, `sin`

and `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
the `icsi_log`

function, while being more precise.

## Left-recursive versus right-recursive lists in LR parsers

- January 21, 2015
- Last updated on 2015/01/22

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.

## Normalization by realizability also computes

- December 2, 2014
- Last updated on 2014/12/02

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.

http://gallium.inria.fr/~scherer/research/norm*by*rea/dagand-scherer-jfla15.pdf