M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, ITP, 2010.
DOI : 10.1007/978-3-642-14052-5_8
URL : https://hal.archives-ouvertes.fr/inria-00502496

F. Baader and T. Nipkow, Term Rewriting and All That, 1998.

J. O. Blech and B. Grégoire, Certifying compilers using higher-order theorem provers as certificate checkers. FMSD, 2011.
DOI : 10.1007/s10703-010-0108-7

S. Boutin, Using reflection to build efficient and certified decision procedures, TACS, 1997.
DOI : 10.1007/BFb0014565

A. Bove and V. Capretta, Computation by Prophecy, TLCA, 2007.
DOI : 10.1007/978-3-540-73228-0_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.105.2242

G. Claret, L. González-huesca, Y. Régis-gianas, and B. Ziliani, Lightweight Proof by Reflection Using a Posteriori Simulation of Effectful Computation, 2013.
DOI : 10.1007/978-3-642-39634-2_8
URL : https://hal.archives-ouvertes.fr/hal-00870110

P. Corbineau, Autour de la clôture de congruence avec coq, ENS, 2001.

G. Gonthier, B. Ziliani, A. Nanevski, and D. Dreyer, How to make ad hoc proof automation less ad hoc, 2011.

B. Grégoire, L. Pottier, and L. Théry, Proof Certificates for Algebra and Their Application to Automatic Geometry Theorem Proving, ADG, 2008.
DOI : 10.1007/978-3-642-21046-4_3

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

D. W. James and R. Hinze, A Reflection-based Proof Tactic for Lattices in Coq, TFP, 2009.

P. Letouzey, Extraction in Coq: An Overview, LTA, 2008.
DOI : 10.1007/978-3-540-69407-6_39
URL : https://hal.archives-ouvertes.fr/hal-00338973

D. Pichardie and V. Rusu, Defining and Reasoning About General Recursive Functions in Type Theory: a Practical Method, 2005.
URL : https://hal.archives-ouvertes.fr/inria-00000910

M. Sozeau, Subset Coercions in Coq, TYPES, 2006.
DOI : 10.1007/978-3-540-74464-1_16
URL : https://hal.archives-ouvertes.fr/inria-00628869

P. Wadler, Comprehending monads, Proceedings of the 1990 ACM conference on LISP and functional programming , LFP '90, 1992.
DOI : 10.1145/91556.91592