Normalization by Evaluation with Free Extensions (Extended Abstract)
summary
Claim: augmenting normalization-by-evaluation with free extensions (frex) produces a single generic NbE algorithm for simply typed lambda calculus with higher-order functions and any primitive type that carries an algebraic theory. Implementation uses a frex interface (homomorphism and unknown injection) to interpret Nat-like types, makes neutrals as unknowns the unknown set, and yields eval/quote and correctness proofs essentially for free. Prototype in OCaml and example extension to a monadic information-flow construct work.
AI-written summary · about