This is an implementation of the NbE Machine as presented in

@Article{Vestergaard:WRS01,
  author =       "Ren{\'e} Vestergaard",
  title =        "The Simple Type Theory of Normalisation by Evaluation",
  booktitle =    "Proceedings of {WRS-1}",
  journal =       "Electronic Notes in Theoretical Computer Science",
  volume =       "57",
  editor =       "Bernhard Gramlich",
  year =         "2001",
  publisher =    "Elsevier Science",
  note =         "Preliminary proceedings are available as technical report
                  number 2001.2359, {D}epartamento de {S}istemas
                  {I}nform{\'a}ticos y {C}omputaci{\'o}n,
                  {U}niversidad {P}olit{\'e}cnica de {V}alencia",
}

***************************************************************************

To use the NbE Machine, do the following:

* download and place all files in a directory
* remove their ".txt" extension
* start (Moscow) ML in that directory
* type "use stt-NbE.sml;" and press <enter>
* run the examples as prescribed in the above article

NB! At present, no parser is available but pretty printing is
fully supported.