D. Delahaye, A Proof Dedicated Meta-Language1 1This work has been realized within the LogiCal project (INRIA-Rocquencourt, France)., Electronic Notes in Theoretical Computer Science, vol.70, issue.2, pp.96-109, 2002.
DOI : 10.1016/S1571-0661(04)80508-5
URL : http://doi.org/10.1016/s1571-0661(04)80508-5

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, $$\lambda $$ Prolog Interpreter, Proceedings of LPAR, 2015.
DOI : 10.1007/978-3-662-48899-7_32

G. Ebner, S. Ullrich, J. Roesch, J. Avigad, and L. De-moura, A metaprogramming framework for formal verification, Proc. ACM Program. Lang. 1, ICFP, pp.34-63, 2017.
DOI : 10.1017/S0956796815000118

G. Malecha and J. Bengtson, Extensible and Efficient Automation Through Reflective Tactics, pp.532-559, 2016.
DOI : 10.1145/2500365.2500579

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
DOI : 10.1017/cbo9781139021326
URL : https://hal.archives-ouvertes.fr/hal-00776197

B. Ziliani, Y. Régis-gianas, and J. Kaiser, The Next 700 Safe Tactic Languages, 2017.