helf alternatives and similar packages
Based on the "Dependent Types" category.
Alternatively, view helf alternatives based on common mentions on social networks and blogs.
-
-
agda-snippets
Library and tool to render the snippets in literate Agda files to hyperlinked HTML, leaving the rest of the text untouched.
InfluxDB - Power Real-Time Data Analytics at Scale
Do you think we are missing an alternative of helf or a related project?
README
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/.