It seemed fitting to begin this new year with greetings to all our beloved readers, before the flood of new posts that will inevitably conquer the world, again.

Sadly, we don’t have anything as great as the OCamllabs 2013 retrospective to give you – I hear there is also an OCamlPro version in the making. As a research group, we actually publish a kind of retrospective called “Rapport d’Activité”. It could be considered boring administrative duty, but is in fact conducted by Xavier with surprising and laudable care. The deadline for the 2013 report is this month, so he’s getting increasingly threatening but we have nothing to show you for now. If you are curious about what it looks like, feel free to go get mesmerized by our 2012 activity report.

On a suggestion by Jonathan, I asked members of Gallium (those that could be contacted by press time) to at least summarize “their professional 2013” in one sentence.

  • Thibaut Balabonski: “Coq, concurrency in Mezzo, pattern calculus in Brasília, more Coq”
  • Arthur Charguéraud: “used OCaml to run an inefficient but formally-proved correct JavaScript interpreter”
  • Pierre Dagand: “Writing in Paris blink Coq/x86 in Cambridge blink LICS in New Orleans blink Viva in Glasgow blink Gaga in Rocquencourt!”
  • Damien Doligez: “release TLA+, release OCaml, release TLA+ (again)”
  • Jacques-Henri Jourdan: “Formalizations in Coq : abstract interpretation, floating point numbers, hash-consing & memoization”
  • Fabrice Le Fessant: “2013 for me: the return to the source”
  • Xavier Leroy: “CompCert grows a new register allocator, 64-bit integers, and some nontrivial static analyses”
  • François Pottier: “Lots of Mezzo, lots of Coq”
  • Jonathan Protzenko: “Mezzo, implementation, writing, ICFP paper”
  • Gabriel Scherer: “Picking a PhD topic and working on it!”

We hope your past year was as fulfilling or more (than, at least, floating point formalization in Coq), and that the next will be even better.