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.
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.
Requires GHC and cabal, for instance via the Haskell Platform. In a shell, type
cabal install helf
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/.