Hackage :: [Package]

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

[ dependent-types, mit, 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]

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

Candidates

Versions [RSS] 0.2016.12.25, 0.2021.8.12
Change log CHANGELOG.md
Dependencies array (>=0.3 && <1.0), base (>=4.6 && <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 MIT
Author Andreas Abel and Nicolai Kraus
Maintainer Andreas Abel <andreas.abel@ifi.lmu.de>
Revised Revision 1 made by AndreasAbel at 2021-08-12T21:33:17Z
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 2021-08-12T21:10:55Z
Distributions NixOS:0.2021.8.12
Executables helf
Downloads 1132 total (10 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
Last success reported on 2021-08-12 [all 1 reports]

Readme for helf-0.2021.8.12

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