Gagallium

Xavier Leroy and I recently submitted a paper about my recent work on a formally-verified alias analysis for CompCert at the Conference on Certified Programs and Proofs (CPP).

This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is intraprocedural, flow-sensitive, field-sensitive, and untyped. Its soundness proof follows the general style of abstract interpretation. The analysis is designed to fit in the CompCert C verified compiler, supporting future aggressive optimizations over memory accesses.

I have recently started an internship in the Gallium team working on intermediate representation (IR) for compilers. The aim is to get a better understanding of the relation that links “traditional” forms and their functional counterparts.

I hope you know about the OCaml Users and Developers Meeting, a continuation of previous years’ “OCaml community meetings” that will be colocated with ICFP in Denmark next September; and that you are considering attending! Some Gallium members will certainly also attend the ML Workshop 2012, another satellite that is less OCaml-focused and maybe more research-oriented than community-oriented. By mere coincidence, it happens that we submitted four different proposals to this workshop. Plenty of activity!

Since there was no easy way to install OCaml under Windows, I set out to write a decent Windows installer. It turns out this was, as expected, not as simple as I expected! In this post, I'll share my experiences with the tool I used, namely NSIS and, hopefully, try to get some readers motivated enough to give me a hand, as there's still room for improvements.