@InProceedings{AbelAehligDybjer07,
  author =       {Abel, Andreas and Aehlig, Klaus and Dybjer, Peter},
  title =        {Normalization by Evaluation for {M}artin-{L}{\"o}f Type
                  Theory with One Universe},
  editor =       {Fiore, M.},
  booktitle =    {Proceedings of the twenty-third Conference on the 
                  Mathematical Foundations of Programming Semantics (MFPS)},
  pages =        {17--39},
  volume =       173,
  series =       {Electronic Notes in Theoretical Computer Science},
  month =        apr,
  year =         2007,
}