The Simple Type Theory of Normalisation by Evaluation

AbstractWe develop the type theory of the Normalisation by Evaluation (NbE) algorithm for the λ-calculus in the simply-typed case. In particular, we show that the algorithm computes long β(η)-normal forms by means of Plotkin's call-by-name and call-by-value β-evaluation semantics. This is noteworthy (i) as the algorithm decides full βη-equality and (ii) as the algorithm so-far only has been presented in model-theoretic terms. To showcase the effective means of the algorithm, we provide an environment machine implementation of the semantics: the NbE Machine. We also analyse the semantics and the environment machine in terms of strategies on the λ-calculus and subsequently address the untyped case. The proof burden is slight