Typechecking terms of the Edinburgh Logical Framework (LF)

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.

helf

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.

Limitations

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.

Installation

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

  cabal install helf

Examples

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/.