So I'm still working on away on typesetting the inference algorithm for InforML. Partly it is because I've decided to just go ahead and do all of it. It has already paid off on illuminating some tricky bits. Additionally, at some stage in my revision I concluded that not only would it be very useful to have higher-rank universal quantification, but that »first-class« existential types would be really handy too.

My initial attempts at this weren't entirely satisfactory, but Stephanie became quite interested in the problem again and worked out her own take on existential inference (kind of a dual to Damas-Milner). So I'm massaging the latest draft of that system in during my current revision cycle.

I expect however I am on my last major pass of revisions before I go back to coding.  If nothing else I'll code up the parts that have become pretty stable to make testing examples stressing the more tenuous bits easier.

Of course, the language has also changed in all sorts of random ways since I last touched the parser, so I may have to spend a bit of time wrestling making the grammar LL(k) approved.  I also have to implement all sorts of operations on graphs, as I'm modeling most of the queries on constraint sets using DAGs.

Anyway, I expect there will be more exciting news to come on the implementation front.