K. Aehlig, F. Haftmann, and T. Nipkow, A Compiled Implementation of Normalization by Evaluation, Theorem Proving in Higher Order Logics Lecture Notes in Computer Science, 2008.
DOI : 10.1007/11532231_4

T. Altenkirch, P. Dybjer, M. Hofmann, and P. Scott, Normalization by evaluation for typed lambda calculus with coproducts, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.203-210, 2001.
DOI : 10.1109/LICS.2001.932506

U. Berger, M. Eberl, and H. Schwichtenberg, Normalization by evaluation. Prospects for Hardware Foundations pp, pp.117-137, 1998.

U. Berger, M. Eberl, and H. Schwichtenberg, Term rewriting for normalization by evaluation, Information and Computation, vol.183, issue.1, pp.19-42, 2003.
DOI : 10.1016/S0890-5401(03)00014-2

F. Blanqui, T. Hardin, and P. Weis, On the Implementation of Construction Functions for Non-free Concrete Data Types, Lecture Notes In Computer Science, vol.4421, p.95, 2007.
DOI : 10.1007/978-3-540-71316-6_8
URL : https://hal.archives-ouvertes.fr/inria-00095110

M. Boespflug, From self-interpreters to normalization by evaluation, Informal proceedings of the 2009 Workshop on Normalization by Evaluation, pp.35-38, 2009.
URL : https://hal.archives-ouvertes.fr/inria-00434284

T. Coquand and P. Dybjer, Intuitionistic model constructions and normalization proofs, Mathematical Structures in Computer Science, vol.7, issue.1, pp.75-94, 1997.
DOI : 10.1017/S0960129596002150

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Lecture Notes in Computer Science, vol.4583, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

P. Crégut, Strongly reducing variants of the Krivine abstract machine, Higher- Order and Symbolic Computation, pp.209-230, 2007.
DOI : 10.1007/s10990-007-9015-z

O. Danvy, Type-directed partial evaluation. POPL'96 pp, pp.242-257, 1996.
DOI : 10.7146/dpb.v24i494.7022
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.291

A. Filinski and H. Rohde, A denotational account of untyped normalization by evaluation, 2004.

G. Gonthier, The Four Colour Theorem: Engineering of a Formal Proof, Lecture Notes in Computer Science, vol.5081, p.333, 2007.
DOI : 10.1007/978-3-540-87827-8_28

B. Grégoire and X. Leroy, A compiled implementation of strong reduction, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming pp, pp.235-246, 2002.

B. Grégoire and A. Mahboubi, Proving equalities in a commutative ring done right in coq. Lecture notes in computer science 3603, p.98, 2005.

L. Fessant, F. Maranget, and L. , Optimizing pattern matching, Proceedings of the sixth ACM SIGPLAN international conference on Functional programming pp, pp.26-37, 2001.

X. Leroy, The ZINC experiment: an economical implementation of the ML language, Tech. rep, p.INRIA, 1990.
URL : https://hal.archives-ouvertes.fr/inria-00070049

J. Lévy, Réductions correctes et optimales dans le Lambda-Calcul, Université Paris, vol.7, 1978.

S. Lindley, Normalisation by evaluation in the compilation of typed functional programming languages, 2005.

S. Marlow and S. Peyton-jones, Making a fast curry: push/enter vs. eval/apply for higher-order languages, Journal of Functional Programming, vol.16, pp.4-5, 2006.