The Twelf implementation comprises
* the LF logical framework, including type reconstruction;
* the Elf constraint logic programming language;
* an inductive meta-theorem prover for LF;
* and an Emacs interface.
Why have you ported 1.4, when 1.5 and even 1.5R1 are available?
My understanding is that 1.5 is a snapshot/working release,
whereas 1.4 is an alpha release, and is thus presumably more
stable. I'd be happy to try porting 1.5R1 if it's important
to track the latest release.