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

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.2016.12.25, 0.2021.8.12, 0.2022.5.30, 1.0.20240318
Change log CHANGELOG.md
Dependencies array (>=0.3 && <1), base (>=4.6 && <5), containers (>=0.3 && <1), mtl (>=2.2.1 && <3), pretty (>=1.0 && <2), QuickCheck (>=2.4 && <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 2022-05-30T09:29:08Z
Distributions NixOS:1.0.20240318
Reverse Dependencies 1 direct, 0 indirect [details]
Executables helf
Downloads 1469 total (18 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 2022-05-30 [all 1 reports]

Readme for helf-0.2022.5.30

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