[. Aehlig, F. Haftmann, and T. Nipkow, A Compiled Implementation of Normalization by Evaluation, LNCS, vol.186, issue.6, pp.39-54, 2008.
DOI : 10.1007/11532231_4

B. Barras and B. Grégoire, On the Role of Type Decorations in the Calculus of Inductive Constructions, Computer Science Logic, pp.151-166, 2005.
DOI : 10.1007/11538363_12

M. Boespflug, Conversion by Evaluation, Proceedings of the Twelfth Internation Symposium on Practical Aspects of Declarative Languages, 2010.
DOI : 10.1007/978-3-642-11503-5_7
URL : https://hal.archives-ouvertes.fr/inria-00434282

S. Boutin, Using reflection to build efficient and certified decision procedures, Theoretical Aspects of Computer Software, pp.515-529, 1997.
DOI : 10.1007/BFb0014565
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.7587

U. Berger and H. Schwichtenberg, An inverse of the evaluation functional for typed lambda -calculus, [1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science, pp.203-211, 1991.
DOI : 10.1109/LICS.1991.151645

T. Coquand and C. Paulin, Inductively defined types, Proceedings of the international conference on Computer logic, pp.50-66, 1990.
DOI : 10.1007/3-540-52335-9_47

O. Danvy, Type-directed partial evaluation, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, POPL '96, 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, Proceedings of the 7th International Conference in Foundations of Software Science and Computation Structures, 2004.

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, Theorem Proving in Higher Order Logics, pp.98-113, 2005.
DOI : 10.1007/11541868_7

G. Gonthier and A. Mahboubi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

]. G. Gon07 and . Gonthier, The four colour theorem: Engineering of a formal proof, Lecture Notes in Computer Science, vol.5081, p.333, 2007.

J. Harrison, Metatheory and reflection in theorem proving: A survey and critique, 1995.

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

]. L. The08 and . Thery, Proof pearl: Revisiting the mini-rubik in coq, Theorem proving in higher order logics: 21st international conference, p.310, 2008.

. Kumar-neeraj, J. Verma, S. Goubault-larrecq, S. Prasad, and . Arun-kumar, Reflecting bdds in coq, LNCS, pp.162-181, 1961.

B. Werner, Une Théorie des Constructions Inductives, p.5, 1994.