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

## How I found a bug in Intel Skylake processors

- July 3, 2017

Instructors of "Introduction to programming" courses know that students are willing to blame the failures of their programs on anything. Sorting routine discards half of the data? "That might be a Windows virus!" Binary search always fails? "The Java compiler is acting funny today!" More experienced programmers know very well that the bug is generally in their code: occasionally in third-party libraries; very rarely in system libraries; exceedingly rarely in the compiler; and never in the processor. That's what I thought too, until recently. Here is how I ran into a bug in Intel Skylake processors while trying to debug mysterious OCaml failures.

## From visitors to iterators

- March 14, 2017

I have been asked whether an automatically-generated visitor, as produced by the visitors syntax extension for OCaml, can be used to construct an iterator.

It turns out that this can be done in a simple and efficient manner. (Up to a constant factor, the time complexity of this solution is optimal.) As the problem is interesting and its solution is somewhat nonobvious, I am describing them here.

## A new blog on the radar!

- February 7, 2017

I am no longer an official member of Gallium, but of course Gallium will always remain dear to my heart. And it is with a mix of sadness and anticipation that I've started writing articles on another blog, namely, the F* blog. If you wish to hear the latest news about F*, and chat about language issues, or just get a sense of what's happening, you can go out there and start lurking in the comments section.

Looking forward to some bikeshedding^W constructive discussions!

## Merging OCaml patches

- August 7, 2015

In Merging OCaml Patches I wrote a description of my personal process to merge OCaml patches (usually submitted as github pull requests) in the upstream repository (currently SVN). This description may be useful for external contributors to understand the process, and maybe meet me halfway by doing a bit of the work upfront.

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