The Simple Type Theory of
            Normalisation by Evaluation

                  Rene Vestergaard


We develop the type theory of the Normalisation by Evaluation
(NbE) algorithm for the lambda-calculus in the simply-typed case.
In particular, we show that the algorithm computes long
beta(eta)-normal forms by means of Plotkin's call-by-name and
call-by-value beta-evaluation semantics. This is noteworthy (i) as
the algorithm decides full beta,eta-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 lambda-calculus and
subsequently address the untyped case. The proof burden is slight.