helf: Typechecking terms of the Edinburgh Logical Framework (LF).

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

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, 0.2021.8.12, 0.2022.5.30, 1.0.20240318, 1.0.20240318
Change log CHANGELOG.md
Dependencies array (>=0.3 && <1), base (>=4.9 && <5), bytestring (>= && <1), containers (>=0.3 && <1), mtl (>=2.2.1 && <3), pretty (>=1.0 && <2), text (>= && <3), transformers (>=0.2 && <1) [details]
License MIT
Author Andreas Abel and Nicolai Kraus
Maintainer Andreas Abel <andreas.abel@ifi.lmu.de>
Category Dependent types
Home page http://www2.tcs.ifi.lmu.de/~abel/projects.html#helf
Source repo head: git clone https://github.com/andreasabel/helf
Uploaded by AndreasAbel at 2024-03-18T18:09:46Z


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for helf-1.0.20240318

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


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