nbe-kripke-racket/README.md

Kripke-style 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.

A more efficient version of NbE based on de Bruijn levels (inverted de bruijn indices) can be found in the debruijn-levels branch.