B. Aydemir, A. Charguéraud, B. C. Pierce, R. Pollack, and S. Weirich, Engineering formal metatheory, 35th ACM Symp. on Principles of Programming Languages, pp.3-15, 2008.
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948

D. Baelde, A linear approach to the proof-theory of least and greatest fixed points, 2008.

D. Baelde, On the Expressivity of Minimal Generic Quantification, International Workshop on Logical Frameworks and Meta- Languages: Theory and Practice ENTCS 228, pp.3-19, 2008.
DOI : 10.1016/j.entcs.2008.12.113
URL : https://hal.archives-ouvertes.fr/inria-00284186

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conf. on Automated Deduction (CADE), LNAI 4603, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

D. Baelde and D. Miller, Least and greatest fixed points in linear logic, International Conference on Logic for Programming and Automated Reasoning (LPAR), volume LNCS 4790, pp.92-106, 2007.

D. Baelde, D. Miller, and Z. Snow, Focused Inductive Theorem Proving, Fifth International Joint Conference on Automated Reasoning, pp.278-292, 2010.
DOI : 10.1007/978-3-642-14203-1_24
URL : https://hal.archives-ouvertes.fr/hal-00772592

D. Baelde, D. Miller, Z. Snow, and A. Viel, Tac: A generic and adaptable interactive theorem prover, 2009.

Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science, 2004.
URL : https://hal.archives-ouvertes.fr/hal-00344237

A. Church, A formulation of the simple theory of types, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

T. Coquand and C. Paulin, Inductively defined types, Conference on Computer Logic, pp.50-66, 1988.
DOI : 10.1007/3-540-52335-9_47

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

A. Gacek, The Abella Interactive Theorem Prover (System Description), Fourth 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. Nadathur, Combining Generic Judgments with Recursive Definitions, 2008 23rd Annual IEEE Symposium on Logic in Computer Science, pp.33-44, 2008.
DOI : 10.1109/LICS.2008.33

A. Gacek, D. Miller, and G. Nadathur, Reasoning in Abella about Structural Operational Semantics Specifications, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp.85-100, 2008.
DOI : 10.1016/j.entcs.2008.12.118

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

J. Girard, A fixpoint theorem in linear logic. An email posting to the mailing list linear@cs, 1992.

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

G. Huet, A unification algorithm for typed ??-calculus, Theoretical Computer Science, vol.1, issue.1, pp.27-57, 1975.
DOI : 10.1016/0304-3975(75)90011-0

C. Liang and D. Miller, Focusing and polarization in linear, intuitionistic, and classical logics, Theoretical Computer Science, vol.410, issue.46, pp.4747-4768, 2009.
DOI : 10.1016/j.tcs.2009.07.041
URL : http://doi.org/10.1016/j.tcs.2009.07.041

R. Mcdowell, Reasoning in a Logic with Definitions and Induction, 1997.

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

R. Mcdowell and D. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002.
DOI : 10.1145/504077.504080

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

D. Miller, Abstract Syntax for Variable Binders: An Overview, Computational Logic -CL 2000, LNAI 1861, pp.239-253
DOI : 10.1007/3-540-44957-4_16

D. Miller, Bindings, mobility of bindings, and the ?-quantifier, 18th International Conference on Computer Science Logic (CSL) 2004, p.24, 2004.

D. Miller, Formalizing Operational Semantic Specifications in Logic, Electronic Notes in Theoretical Computer Science, vol.246, 2008.
DOI : 10.1016/j.entcs.2009.07.020

D. Miller, G. Nadathur, F. Pfenning, and A. Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

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

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

A. Momigliano and A. Tiu, Induction and Co-induction in Sequent Calculus, Post-proceedings of TYPES 2003, pp.293-308, 2003.
DOI : 10.1007/978-3-540-24849-1_19

G. Nadathur and D. Miller, An Overview of ?Prolog, Fifth International Logic Programming Conference, pp.810-827, 1988.

G. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, 16th Conf. on Automated Deduction (CADE), LNAI 1632, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

T. Nipkow, L. C. Paulson, and M. Wenzel, Isabelle/HOL: A Proof Assistant for Higher-Order Logic, LNCS Tutorial, vol.2283, 2002.
DOI : 10.1007/3-540-45949-9

F. Pfenning and C. Elliott, Higher-order abstract syntax, Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, 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), LNAI 1632, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

B. Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08), pp.371-382, 2008.

A. Poswolsky and C. Schürmann, System Description: Delphin ??? A Functional Programming Language for Deductive Systems, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp.113-120, 2008.
DOI : 10.1016/j.entcs.2008.12.120

P. Schroeder-heister, Cut-elimination in logics with definitional reflection, Nonclassical Logics and Information Processing, pp.146-171, 1992.
DOI : 10.1007/BFb0031929

P. Schroeder-heister, Rules of definitional reflection, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.222-232, 1993.
DOI : 10.1109/LICS.1993.287585

C. Schürmann, Automating the Meta Theory of Deductive Systems, 2000.

A. Tiu, A Logical Framework for Reasoning about Logical Specifications, 2004.

A. Tiu, Model Checking for ??-Calculus Using Proof Search, CONCUR, pp.36-50, 2005.
DOI : 10.1007/11539452_7

A. Tiu and D. Miller, Proof search specifications of bisimulation and modal logics for the ??-calculus, ACM Transactions on Computational Logic, vol.11, issue.2, p.2010
DOI : 10.1145/1656242.1656248

C. Urban, Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.323, issue.1???2, pp.327-356, 2008.
DOI : 10.1007/s10817-008-9097-2