Hackage :: [Package]

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

[ 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 LicenseRef-OtherLicense
Author Andreas Abel and Nicolai Kraus
Maintainer Andreas Abel <andreas.abel@ifi.lmu.de>
Revised Revision 1 made by HerbertValerioRiedel at Sun Dec 25 21:06:23 UTC 2016
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 Sun Dec 25 20:48:23 UTC 2016
Distributions NixOS:0.2016.12.25
Executables helf
Downloads 353 total (8 in the last 30 days)
Rating (no votes yet) [estimated by rule of succession]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2016-12-26 [all 3 reports]
Hackage Matrix CI

Downloads

Note: This package has metadata revisions in the cabal description newer than included in the tarball. To unpack the package including the revisions, use 'cabal get'.

Maintainer's Corner

For package maintainers and hackage trustees

Readme for helf-0.2016.12.25

[back to package description]

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