D. Delahaye, A Tactic Language for the System Coq, LPAR, pp.85-95, 1955.
DOI : 10.1007/3-540-44404-1_7
URL : https://hal.archives-ouvertes.fr/hal-01125070

A. Felty and A. Momigliano, Hybrid, Journal of Automated Reasoning, vol.18, issue.1, pp.43-105, 2012.
DOI : 10.1007/s10817-010-9194-x

A. P. Felty, A. Momigliano, and B. Pientka, The next 700 challenge problems for reasoning with higherorder abstract syntax representations: Part 1?A foundational view, 2014.

A. P. Felty, A. Momigliano, and B. Pientka, The next 700 challenge problems for reasoning with higherorder abstract syntax representations: Part 2?A survey, 2014.

A. Gacek, The Abella Interactive Theorem Prover (System Description), Proceedings of the International Joint Conference on Automated Reasoning, pp.154-161, 2008.
DOI : 10.1007/978-3-540-71070-7_13

A. Gacek, A Framework for Specifying, Prototyping, and Reasoning about Computational Systems, 2009.

A. Gacek, D. Miller, and G. , Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004
URL : http://doi.org/10.1016/j.ic.2010.09.004

A. Gacek, D. Miller, and G. Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-011-9218-1
URL : https://hal.archives-ouvertes.fr/hal-00776208

D. Miller and G. Nadathur, A computational logic approach to syntax and semantics, Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, 1985.

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

D. Miller and A. Tiu, A proof theory for generic judgments: an extended abstract, 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp.118-127, 2003.
DOI : 10.1109/LICS.2003.1210051

A. Nanevski, F. Pfenning, and B. Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, pp.1-49, 2008.
DOI : 10.1145/1352582.1352591
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.1028.3796

F. Pfenning and C. Elliott, Higher-order abstract syntax, PLDI, pp.199-208, 1988.

F. Pfenning and C. Schuermann, Twelf User's Guide, 2002.

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

B. Pientka and J. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), IJCAR, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2

X. Qi, A. Gacek, S. Holte, G. Nadathur, and Z. Snow, The Teyjus system ? version 2, 2008.

C. Urban, A. M. Pitts, and M. Gabbay, Nominal unification, Theoretical Computer Science, vol.323, issue.1-3, pp.473-497, 2004.
DOI : 10.1016/j.tcs.2004.06.016

Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur, Reasoning about higher-order relational specifications, Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pp.157-168, 2013.
DOI : 10.1145/2505879.2505889
URL : https://hal.archives-ouvertes.fr/hal-00787126