SML source. probably inscrutable if you aren't me, though there are comments.
Demonstration file. It can be executed but is really meant to be read -- it contains an explanation of the syntax for propositional functions that I use (but you should look at the subsequent paper for additional info about variable binding, which is rather peculiar!) and then contains examples of checker commands with their expected output.
The first draft of a paper on the formalization of RTT (and a related simple type theory). The paper is now basically complete, though I think it still needs a little polish.
In the SML source, there is also source and some examples of the RTT proof checker under construction, but I'm not talking about that quite yet.
There is an NFP connection...
This work was inspired by my reading of an now published paper of Kamareddine, Nederpelt, and Laan, though the approach I take to formalizing the type theory of the ramified theory of types is quite different from theirs. I use a modified form of their formalized syntax for RTT.