InforML Complete

Department espresso machine mortally wounded

It has taken nearly ten months, and numerous changes in direction, but I am finally declaring my implementation of the InforML language as complete. Or at least as complete as I am planning on making it, modulo bug fixing and polishing that arises while I work on the examples I will be including in my dissertation.

Since I last wrote about InforML, which to my surprise has been exactly a month, I've fleshed out remaining details concerning typechecking and implemented a simple compiler to mzscheme. At Stephanie's suggestion, I also took a day or so and implemented some simple local type inference, which takes care of quite a few of the label and type applications that were previously required.

Typechecking actually became problematic as Twelf proved to have very unpredictable behavior on very similar queries. Just changing a single label in a query would cause it to diverge. I eventually even discovered a bug that was causing the theorem prover to claim proofs of clearly unsolvable queries. At least I see no way they could be proved and the Twelf tabled logic programming engine agreed that there were no solutions. So even if I am wrong and they may be proven, either the theorem prover or the tabled logic programming engine cannot both be correct. Right now I am betting on the prover being wrong because doesn't generate proof terms. To help with both of these issues, I wrote a number of custom constraint and subsumption solvers in SML that handle the vastly more common case where the problems are entirely constrained to ground labels, kinds, types, and signatures.

So now I am beginning to mostly focus on the actual writing of my dissertation along with studying idioms and methodologies for programming in InforML. My current timeline calls for this phase to be completed by the beginning of September, which seems believable.


  1. Dan Vogel said,

    July 2, 2007 @ 10:24 am

    Congratulations on finishing InforML… finally.

  2. washburn said,

    July 2, 2007 @ 2:59 pm

    Thanks. Of course, I still have a few more »finally«s to go before November. It will be nice to move onto some projects that aren’t building throwaway prototypes.

  3. James Cheney said,

    July 19, 2007 @ 9:14 am

    Is that the Peter Buneman Memorial Coffee Machine on the fritz?!

  4. washburn said,

    July 19, 2007 @ 9:17 am

    Yes, that is the Peter Buneman Memorial Coffee Machine. However, fortunately Cheryl was able to work some magic and get it running again the following day. That said, it is used much more heavily than its manufactured specs, so it is probably only a matter of time before we need the Peter Buneman Memorial Coffee Machine Memorial Coffee Machine.

  5. James Cheney said,

    July 22, 2007 @ 2:03 pm

    Tell me about it. We have a similar one here (just for our floor, about 20-25 people) and it breaks down once a year – we have to send it in to the manufacturer to replace the coffee bean grinder.

RSS feed for comments on this post · TrackBack URI

Leave a Comment