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
DOI : 10.1109/LICS.2001.932506

U. Berger, M. Eberl, and H. Schwichtenberg, Normalization by evaluation. Prospects for Hardware Foundations, pp.117-137, 1998.
DOI : 10.1007/3-540-49254-2_4
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.128.5124

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
URL : http://doi.org/10.1016/s0890-5401(03)00014-2

T. Blanqui, P. Hardin, and . 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

C. Coquand, From semantics to rules: A machine assisted analysis, Lecture Notes In Computer Science, pp.91-91, 1994.
DOI : 10.1007/BFb0049326
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.5491

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.

O. Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 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. K. 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.235-246, 2002.

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

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

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

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

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

L. Maranget, Compiling pattern matching to good decision trees, Proceedings of the 2008 ACM SIGPLAN workshop on ML, ML '08, pp.35-46, 2008.
DOI : 10.1145/1411304.1411311

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

F. Pfenning and C. Elliot, Higher-order abstract syntax, Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation -PLDI '88, pp.199-208, 1988.