Typeful Normalization by Evaluation

Olivier Danvy, Chantal Keller, Matthias Puech. Typeful Normalization by Evaluation. In Hugo Herbelin, Pierre Letouzey, Matthieu Sozeau, editors, 20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France. Volume 39 of LIPIcs, pages 72-88, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2014. [doi]

@inproceedings{DanvyKP14,
  title = {Typeful Normalization by Evaluation},
  author = {Olivier Danvy and Chantal Keller and Matthias Puech},
  year = {2014},
  doi = {10.4230/LIPIcs.TYPES.2014.72},
  url = {http://dx.doi.org/10.4230/LIPIcs.TYPES.2014.72},
  researchr = {https://researchr.org/publication/DanvyKP14},
  cites = {0},
  citedby = {0},
  pages = {72-88},
  booktitle = {20th International Conference on Types for Proofs and Programs, TYPES 2014, May 12-15, 2014, Paris, France},
  editor = {Hugo Herbelin and Pierre Letouzey and Matthieu Sozeau},
  volume = {39},
  series = {LIPIcs},
  publisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
  isbn = {978-3-939897-88-0},
}