Gagallium

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.

http://gallium.inria.fr/~scherer/drafts/2-or-more-approximation.pdf

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