U. Norell, Towards a practical programming language based on dependent type theory, pp.412-96, 2007.

U. Norell, Dependently typed programming in Agda In: Proceedings of the 4th international workshop on Types in language design and implementation. TLDI '09, pp.1-2, 2009.

P. Van-der-walt, Reflection in Agda Master's thesis The Netherlands (2012) available online

K. M. Pitman, Special forms in Lisp, Proceedings of the 1980 ACM conference on LISP and functional programming , LFP '80, pp.179-187, 1980.
DOI : 10.1145/800087.802804

W. Taha and T. Sheard, Multi-stage programming with explicit annotations, Proceedings of the 1997 ACM SIGPLAN symposium on Partial evaluation and semanticsbased program manipulation. PEPM '97, 1997.

T. Sheard, P. Jones, and S. , Template meta-programming for Haskell, Proceedings of the 2002 ACM SIGPLAN workshop on Haskell, pp.1-16, 2002.

P. Martin-löf, Constructive Mathematics and Computer Programming, Proc. of a discussion, pp.167-184, 1985.
DOI : 10.1016/S0049-237X(09)70189-2

T. Coquand and G. P. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

N. Oury and W. Swierstra, The power of pi, Proceedings of the 13th ACM SIGPLAN international conference on Functional programming. ICFP '08, pp.39-50, 2008.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Chlipala, Certified programming with dependent types, 2011.

W. Jedynak, Agda ring solver using reflection. online, GitHub, https://github. com/wjzz/Agda-reflection-for-semiring-solver (2012) [Online; accessed 26, 2012.

F. Demers and J. Malenfant, Reflection in logic, functional and object-oriented programming: a short comparative study, Proceedings of the IJCAI, pp.29-38, 1995.

B. C. Smith, Reflection and semantics in LISP, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '84, pp.23-35, 1984.
DOI : 10.1145/800017.800513

A. Stump, Directly reflective meta-programming. Higher-Order and Symbolic Computation, pp.115-144, 2009.

A. Goldberg and D. Robson, Smalltalk-80: the language and its implementation, 1983.

T. Sheard, Staged programming. online, 2012.

T. Altenkirch, [Agda mailing list] More powerful quoting and reflection? mailing list communicationonline; accessed 14, 2012.

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, Journal of Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

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