Typechecking terms of the Edinburgh Logical Framework (LF). http://www2.tcs.ifi.lmu.de/~abel/projects.html#helf

Latest on Hackage:0.2016.12.25

This package is not currently in any snapshots. If you're interested in using it, we recommend adding it to Stackage Nightly. Doing so will make builds more reliable, and allow stackage.org to host generated Haddocks.

OtherLicense licensed by Andreas Abel and Nicolai Kraus
Maintained by Andreas Abel


A Haskell implementation of the Edinburgh Logical Framework.

helf parses and typechecks .elf files written for the Twelf implementation of the Logical Framework. helf is mainly a laboratory to experiment with different representation of lambda-terms for bidirectional typechecking.


helf only understands a subset of the Twelf language and implements only a small subset of Twelf's features. + helf does not parse the backarrow <- notation for function space. + helf only understands the fixity pragmas for operators. It ignores all other pragmas. + helf only implements bidirectional type checking. It does not have unification or type reconstruction. + helf does not give nice error messages.


Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type

  cabal install helf


File eval.elf:

% Untyped lambda calculus.

tm   : type.
abs  : (tm -> tm) -> tm.
app  : tm -> (tm -> tm).

% cbn weak head evaluation.

eval : tm -> tm -> type.

eval/abs : {M : tm -> tm}
  eval (abs M) (abs M).

eval/app : {M : tm} {M' : tm -> tm} {N : tm} {V : tm}
  eval M (abs M') ->
  eval (M' N) V   ->
  eval (app M N) V.

Type check with:

  helf eval.elf

For more examples, see test/succeed/.

comments powered byDisqus