O. Savary-bélanger and K. Chaudhuri, Automatically deriving schematic theorems for dynamic contexts, LFMTP '14, pp.1-9, 2014.

A. Cave and B. Pientka, Programming with binders and indexed data-types, POPL, pp.413-424, 2012.

A. Felty and D. Miller, Encoding a dependent-type ??-calculus in a logic programming language, CADE, volume 449 of LNAI, 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

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

D. Miller and G. Nadathur, A computational logic approach to syntax and semantics. 10th Symp, of the Mathematical Foundations of Computer Science, 1985.

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

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Transactions on Computational Logic, vol.6, issue.4, pp.749-783, 2005.
DOI : 10.1145/1094622.1094628

G. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, CADE, number 1632 in Lecture Notes in Artificial Intelligence, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

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. 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), IJCAR, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2

A. Poswolsky and C. Schürmann, System Description: Delphin ??? A Functional Programming Language for Deductive Systems, Electronic Notes in Theoretical Computer Science, vol.228, pp.113-120, 2008.
DOI : 10.1016/j.entcs.2008.12.120

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 G. Nadathur, A ?Prolog based animation of Twelf specifications, 2014.

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