The Polymorphic Type Theory of
              Normalisation by Evaluation

                  Rene Vestergaard

We present the type theory of Normalisation by Evaluation for
System F in the form of a two-level calculus: System F^NbE. System
F^NbE only has redexes in one level and does not allow contraction
under abstractions in that level, i.e., it _evaluates_ terms.
System FNbE is confluent and strongly normalising and its normal
forms are the long beta(eta)-normal forms of System F. We go on to
present a renaming-free environment machine which implements
System F^NbE (in ML).