No description
|
||
---|---|---|
.woodpecker.yaml | ||
nbe-test.rkt | ||
nbe.rkt | ||
README.md |
untyped NbE in racket
An implementation of normalization by evaluation loosely based on A Denotational Account of Untyped Normalization by Evaluation and Abel's thesis on NbE.
Since the implementation is untyped, the normalize
function only
gives you β-normal forms. However, you can get a little bit of
βη-equivalence by invoking Coquand's algorithm (η-eq?
) on
β-normal forms.