HELF = Haskell implementation of the Edinburgh Logical Framework HELF implements only a subset of the Twelf syntax and functionality. It type-checks LF definitions, but does not do type reconstruction.