Jason (jcreed) wrote,

After Doing the Improbable (got the not-so-great TPHOLs class-B paper accepted, whee) I have, on a completely unrelated note, begun Doing the Probably Not A Great Idea, namely trying to write an LF typechecker off the cuff in Java, because this task was suggested as something that would be useful in a meeting today involving Frank and a guy over in ECE interested in proof-carrying authentication, especially the benefits a PCA system would have to teaching security protocols - it would make experimentation somewhat easier. In any event, portability (i.e. to little handheld devices) is of paramount importance for one of the applications, so he thought Java would be a good implementation language.
Not that I would instinctively agree or anything, but I was really curious (a) exactly how bad/not-so-bad Java would be for something very natural to code in ML and (b) exactly how trivial it would be to turn the algorithmic typechecker Frank and Bob's Canonical Forms in LF paper into code. Oh, the other main issue is that proofs in PCA are fairly small compared to PCC, so optimizing the hell out of the proof checker isn't so important - the naive algorithm (the one I'm trying to implement) should be okay.

After a few hours of hacking and remembering Java, I have a little parser, translation into deBruijn indices, and substitution apparently working. The one major bug that came up involved, of course, side-effects and pointer-sharing; there were two integer container classes that were actually the same, and a shift substitution that incremented the same index twice when trying to compute (\x \y x x)[^]. Hooray for non-functional languages! Grr. Well, that's only been a mild obstacle. I think I'll soon have a feel for how painful it is to implement the real stuff.
  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded