The helf package

[ Tags: dependent-types, program ] [ Propose Tags ]

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.

[Skip to Readme]


Versions 0.2016.12.25
Dependencies array (>=0.3 && <1.0), base (>=4.2 && <5.0), containers (>=0.3 && <1.0), mtl (>=2.2.1 && <3.0), pretty (>=1.0 && <2.0), QuickCheck (>=2.4 && <3.0) [details]
License OtherLicense
Author Andreas Abel and Nicolai Kraus
Maintainer Andreas Abel <>
Category Dependent types
Home page
Source repository head: git clone
Uploaded Sun Dec 25 20:48:23 UTC 2016 by AndreasAbel
Updated Sun Dec 25 21:06:23 UTC 2016 by HerbertValerioRiedel to revision 1
Distributions NixOS:0.2016.12.25
Executables helf
Downloads 87 total (11 in the last 30 days)
Rating 0.0 (0 ratings) [clear rating]
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2016-12-26 [all 3 reports]
Hackage Matrix CI


Maintainer's Corner

For package maintainers and hackage trustees

Readme for helf-0.2016.12.25

[back to package description]


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