A. Abel, J. Öhman, and A. Vezzosi, Decidability of conversion for type theory in type theory, PACMPL, vol.2, p.29, 2018.

T. Altenkirch and A. Kaposi, Type theory in type theory using quotient inductive types, vol.16, pp.18-29, 2016.

A. Anand and G. Morrisett, Revisiting Parametricity: Inductives and Uniformity of Propositions, CoqPL'18, 2018.

A. Anand, A. Appel, G. Morrisett, Z. Paraskevopoulou, R. Pollack et al., CertiCoq: A verified compiler for Coq, 2017.

M. Armand, B. Grégoire, A. Spiwack, and L. Théry, Extending Coq with Imperative Features and Its Application to SAT Verification, Interactive Theorem Proving, pp.83-98, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00502496

B. Barras, Auto-validation d'un système de preuves avec familles inductives, vol.7, 1999.

J. P. Bernardy, P. Jansson, and R. Paterson, Proofs for free: Parametricity for dependent types, Journal of Functional Programming, vol.22, issue.2, pp.107-152, 2012.

S. Boulier, P. M. Pédrot, and N. Tabareau, The next 700 syntactical models of type theory, CPP'17, pp.182-194, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01445835

J. Chapman, Type Theory Should Eat Itself, Electronic Notes in Theoretical Computer Science, vol.228, pp.21-36, 2008.

A. Chlipala, Certified Programming with Dependent Types, Introduction to algorithms, 2009.

D. Devriese and F. Piessens, Typed syntactic meta-programming, Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ACM, ICFP '13, 2013.

G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and M. De, A Metaprogramming Framework for Formal Verification, Proceedings of the 22st ACM SIGPLAN Conference on Functional Programming, vol.34, p.29, 2017.

Y. Forster and F. Kunze, Verified Extraction from Coq to a Lambda-Calculus, Coq Workshop, 2016.

Y. Forster and F. Kunze, A certifying extraction with time bounds from coq to call-byvalue ?-calculus, p.11818, 1904.

Y. Forster and G. Smolka, Weak call-by-value lambda calculus as a model of computation in Coq, pp.189-206, 2017.

H. Herbelin and A. Spiwack, The rooster and the syntactic bracket, 19th International Conference on Types for Proofs and Programs, TYPES 2013, vol.26, pp.169-187, 2013.
URL : https://hal.archives-ouvertes.fr/hal-01097919

G. Jaber, G. Lewertowski, P. M. Pédrot, M. Sozeau, and N. Tabareau, The definitional side of the forcing, LICS'16, pp.367-376, 2016.
URL : https://hal.archives-ouvertes.fr/hal-01319066

J. M. Jansen, Programming in the ?-calculus: From Church to Scott and back, The Beauty of Functional Code, vol.8106, pp.168-180, 2013.

C. Keller and M. Lasson, Parametricity in an impredicative sort, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00730913

M. Lasson, Canonicity of Weak ?-groupoid Laws Using Parametricity Theory, Proceedings of the 30th Conference on the Mathematical Foundations of Programming Semantics, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01105252

G. Malecha and J. Bengtson, Extensible and efficient automation through reflective tactics, ESOP 2016, 2016.

G. M. Malecha, Extensible proof engineering in intensional type theory, 2014.

T. Mogensen, Efficient self-interpretations in lambda calculus, J Funct Program, vol.2, issue.3, pp.345-363, 1992.

E. Mullen, S. Pernsteiner, J. R. Wilcox, Z. Tatlock, and D. Grossman, OEuf: minimizing the coq extraction TCB, Proceedings of CPP 2018, pp.172-185, 2018.

P. Pédrot and N. Tabareau, An effectful way to eliminate addiction to dependence, LICS'17, pp.1-12, 2017.

J. C. Reynolds, Types, abstraction and parametric polymorphism, pp.513-523, 1983.

T. Sheard and S. P. Jones, Template meta-programming for haskell, SIGPLAN Not, vol.37, issue.12, pp.60-75, 2002.

T. Sheard and S. P. Jones, Template meta-programming for haskell, Proceedings of the, pp.1-16, 2002.

M. Sozeau, Program-ing Finger Trees in Coq, pp.13-24, 2007.

W. Taha and T. Sheard, Multi-stage programming with explicit annotations, pp.203-217, 1997.

P. Wadler, Theorems for free! In: Functional Programming Languages and Computer Architecture, pp.347-359, 1989.

P. Van-der-walt and W. Swierstra, Engineering Proof by Reflection in Agda, Implementation and Application of Functional Languages, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00987610

B. Ziliani and M. Sozeau, Comprehensible Guide to a New Unifier for CIC Including Universe Polymorphism and Overloading, Journal of Functional Programming, vol.27, p.10, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01671925

B. Ziliani, D. Dreyer, N. R. Krishnaswami, A. Nanevski, and V. Vafeiadis, Mtac: A Monad for Typed Tactic Programming in Coq, Journal of Functional Programming, vol.25, 2015.