No description
Find a file
2025-05-12 00:58:49 -04:00
.woodpecker.yaml Add README.md 2025-04-29 18:17:49 -04:00
nbe-test.rkt Finish adding natural numbers 2025-05-12 00:48:47 -04:00
nbe.rkt Finish adding natural numbers 2025-05-12 00:48:47 -04:00
README.md Update the README file 2025-05-12 00:58:49 -04:00

untyped NbE in racket

status-badge

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.