Anyhow, it just reminded me of HOL-Light, the tool he uses to do his formalization in, and how simple it is supposed to be for having only a 1,000 loc "trusted computing base", that being a 1,000 line C program, I think. It got me wondering how much effort and code it would really take, comparatively, to hack up just a canonical-forms LF typechecker, a task whose easiness has long been a rule of thumb, and it turned out the thumb was right. About two hours of hacking, and 125 lines of ML. It even fits on one screen if I take out all the whitespace:
It's probably not very efficient at all, since I implemented contexts and signatures very naively, and it has a funny input syntax to make parsing relatively trivial. Still, proof of concept.
