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]

Properties

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 (>=0.10.0.0 && <1), containers (>=0.3 && <1), mtl (>=2.2.1 && <3), pretty (>=1.0 && <2), text (>=1.0.0.1 && <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

Downloads

helf-1.0.20240318.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

Package maintainers

AndreasAbel

For package maintainers and hackage trustees

edit package information

Readme for helf-1.0.20240318

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