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!

The proposals are only two pages long, so you should feel free to have a look, react, and ask questions. Please keep in mind that they describe work in progress, and are therefore maybe not as polished as your usual research article.

Jonathan Protzenko and François Pottier submitted a talk proposal about Hamlet, a new programming language they are working on. Hamlet provides fine-grained control over state mutation by tracking aliasing and ownership of state, without being so complex that only type system researchers can use it. In case you want to know more about Hamlet, they have already written an introduction to Hamlet (PDF, 20 pages), also available in a long version (PDF, 27 pages).

Jacques Garrigue and Didier Rémy submitted a proposal about inference for GADT (which were very recently added to OCaml). Doing inference in presence of GADT is difficult because of ambiguities that may arise; in particular, principality is in danger. There has been active research on this problem, with works for example by Simonet and Pottier (2004), Struckey and Sulzmann (2005), Régis-Gianas and Pottier (2006), Peyton-Jones, Vytiniotis, Weirich and Washburn (2004-2006) and finally Schrijvers, Peyton-Jones, Sulzmann, and Vytiniotis (2009). Jacques and Didier are considering a new technique, based on a finer-grained notion of ambiguity, that is quite lightweight and integrates well with the current type system implementation.

Xavier Clerc (whom we are lucky to have as a part-time research engineer) sent a proposal about his recent progress on the OCaml-Java project, which is quite impressive. OCaml-Java compiles OCaml programs to run on the Java Virtual Machine, and provides an interoperability layer to interact at runtime with Java objects. It used to take a very large performance hit compared to the existing native or bytecode compilers, but recent work by Xavier has made it much more competitive, joining the select club of third-party compilers that stand between native and bytecode compilation, whose only members were, as far as I know, OCamlJIT and js_of_ocaml.

Finally, Didier and I submitted another proposal about GADT, this time focused on its interaction with subtyping, and in particular the variance check for type parameters of a GADT declaration. This is the result of questions I have stumbled upon mostly by chance (or misfortune) and asked on the mailing-list; it turns out there has been little work on combining GADT and subtyping (Vincent Simonet did a bit of that with François, and their paper is a great help). Since this mailing-list discussion I have done a bit of formal work, but it does not appear in the proposal. In fact, formal criteria used to be present, until Jonathan and Jacques-Henri most helpfully pointed out that it was impossible to understand (given the space constraints rather than my writing style, I hope). I went for an example-oriented approach which is, I think, much better.

Summing up, and hot off the press:

Of course, some of these proposals may be rejected. That’s the point of celebrating when you submit something rather than once you get the reviews back: you don’t get to rejoice in front of your colleague in tears. In any case, you will probably hear about these works again in the future, if you are interested.