23 references, page 1 of 3
[1] The Abella prover, 2013. Available at http://abella-prover.org/.

[2] B. Accattoli. Proof pearl: Abella formalization of lambda calculus cube property. In C. Hawblitzel and D. Miller, editors, Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS, pages 173-187. Springer, 2012.

[3] J. Cheney and C. Urban. Alpha-Prolog: A logic programming language with names, binding, and alpha-equivalence. In B. Demoen and V. Lifschitz, editors, Logic Programming, 20th International Conference, volume 3132 of LNCS, pages 269-283. Springer, 2004.

[4] J. Cheney and C. Urban. Nominal logic programming. ACM Trans. Program. Lang. Syst., 30(5):1-47, 2008.

[5] A. Church. A formulation of the simple theory of types. J. of Symbolic Logic, 5:56-68, 1940.

[6] N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem. Indagationes Mathematicae, 34(5):381-392, 1972.

[7] A. Felty and D. Miller. Encoding a dependent-type λ-calculus in a logic programming language. In M. Stickel, editor, Proceedings of the 1990 Conference on Automated Deduction, volume 449 of LNAI, pages 221-235. Springer, 1990.

[8] A. Felty and A. Momigliano. Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax. J. of Automated Reasoning, 48:43-105, 2012.

[9] A. Gacek. A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. PhD thesis, University of Minnesota, 2009.

[10] A. Gacek, D. Miller, and G. Nadathur. Nominal abstraction. Information and Computation, 209(1):48-73, 2011.