The helf package

[Tags:program]

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]

Properties

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 <andreas.abel@ifi.lmu.de>
Category Dependent types
Home page http://www2.tcs.ifi.lmu.de/~abel/projects.html#helf
Source repository head: git clone https://github.com/andreasabel/helf
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
Downloads 40 total (7 in the last 30 days)
Votes
0 []
Status Docs not available [build log]
Last success reported on 2016-12-26 [all 3 reports]

Downloads

Maintainer's Corner

For package maintainers and hackage trustees

Readme for helf

Readme for helf-0.2016.12.25

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