D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, p.2014
URL : https://hal.archives-ouvertes.fr/hal-01102709

A. Felty and D. Miller, Encoding a dependent-type ??-calculus in a logic programming language, Conference on Automated Deduction, pp.221-235, 1990.
DOI : 10.1007/3-540-52885-7_90
URL : https://hal.archives-ouvertes.fr/inria-00075299

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

A. Gacek, D. Miller, and G. Nadathur, Nominal abstraction. Information and Computation, 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

F. Harper, G. Honsell, and . Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060

R. Harper and D. R. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.613-673, 2007.
DOI : 10.1006/inco.2001.2951

R. Mcdowell and D. Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, issue.1-2, pp.91-119, 2000.
DOI : 10.1016/S0304-3975(99)00171-1

. Miller, Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, issue.4, pp.321-358, 1992.
DOI : 10.1016/0747-7171(92)90011-R

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, 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), Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2

Z. Snow, D. Baelde, and G. Nadathur, A meta-programming approach to realizing dependently typed logic programming, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.187-198, 2010.
DOI : 10.1145/1836089.1836113

M. Southern and K. Chaudhuri, A two-level logic approach to reasoning about typed specification languages, 34th Int. Conf. on Foundations of Software Technology and Theoretical Computer Science (FSTTCS), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs), pp.557-569, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091544

R. Virga, Higher-order Rewriting with Dependent Types, 1999.

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

K. Watkins, I. Cervesato, F. Pfenning, and D. Walker, A concurrent logical framework I: Judgments and properties 18 The Abella web-site, 2003.