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

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

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, D. Miller, and C. Palamidessi, Encoding transition systems in sequent calculus, Theoretical Computer Science, vol.294, issue.3, pp.411-437, 2003.
DOI : 10.1016/S0304-3975(01)00168-2

A. Momigliano and A. Tiu, Induction and co-induction in sequent calculus Post-proceedings of TYPES, LNCS, issue.3085, pp.293-308, 2003.

A. Tiu, A logical framework for reasoning about logical specifications, 2004.

R. Milner, Communicating and Mobile Systems : The ?-calculus, 1999.

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

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, Abstract Syntax for Variable Binders: An Overview, Computational Logic -CL 2000, no. 1861 in LNAI, pp.239-253, 2000.
DOI : 10.1007/3-540-44957-4_16

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.

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

F. Pfenning and C. Schürmann, System Description: Twelf ??? A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE), no. 1632 in LNAI, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

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

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), no. 4603 in LNAI, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

A. Tiu, A Logic for Reasoning about Generic Judgments, Int. Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP'06), pp.3-18, 2006.
DOI : 10.1016/j.entcs.2007.01.016

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. M. Pitts, Nominal logic, a first order theory of names and binding, Information and Computation, vol.186, issue.2, pp.165-193, 2003.
DOI : 10.1016/S0890-5401(03)00138-X

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
URL : http://arxiv.org/abs/0802.0865

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. Tiu and D. Miller, A Proof Search Specification of the ??-Calculus, 3rd Workshop on the Foundations of Global Ubiquitous Computing, pp.79-101, 2004.
DOI : 10.1016/j.entcs.2005.05.006

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

D. 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

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

A. Tiu and A. Momigliano, Induction and co-induction in sequent calculus, p.4727, 2009.

A. Tiu, Cut elimination for a logic with generic judgments and induction, Tech. rep., CoRR, extended version of LFMTP'06 paper Available from http, p.3065, 2008.

W. W. Tait, Intensional interpretations of functionals of finite type I, The Journal of Symbolic Logic, vol.91, issue.02, pp.198-212, 1967.
DOI : 10.1007/BF01447860

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

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
DOI : 10.1145/1656242.1656248

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

J. Cheney and C. Urban, Nominal logic programming, ACM Transactions on Programming Languages and Systems, vol.30, issue.5, pp.1-47, 2008.
DOI : 10.1145/1387673.1387675
URL : http://arxiv.org/abs/cs/0609062

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

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, pp.3-19, 2008.

J. Cheney, A Simpler Proof Theory for Nominal Logic, 8th International Conference on the Foundations of Software Science and Computational Structures (FOSSACS), pp.379-394, 2005.
DOI : 10.1007/978-3-540-31982-5_24

M. Gabbay, Fresh Logic: proof-theory and semantics for FM and nominal techniques, Journal of Applied Logic, vol.5, issue.2, pp.356-387, 2007.
DOI : 10.1016/j.jal.2005.10.012

A. Gacek, Relating nominal and higher-order abstract syntax specifications, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.177-186, 2010.
DOI : 10.1145/1836089.1836112
URL : http://arxiv.org/abs/1003.5447

J. Cheney, Equivariant unification, Journal of Automated Reasoning
DOI : 10.1007/s10817-009-9164-3
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.59.2544

A. M. Pitts, Alpha-structural recursion and induction, Journal of the ACM, vol.53, issue.3, pp.459-506, 2006.
DOI : 10.1145/1147954.1147961
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.518

B. Aydemir, A. Bohannon, and S. Weirich, Nominal Reasoning Techniques in Coq, Electronic Notes in Theoretical Computer Science, vol.174, issue.5, pp.69-77, 2006.
DOI : 10.1016/j.entcs.2007.01.028

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

R. Mcdowell, Reasoning in a logic with definitions and induction, 1997.

A. Gacek, A framework for specifying, prototyping, and reasoning about computational systems, 2009.

C. Schürmann and F. Pfenning, Automated theorem proving in a simple meta-logic for LF, 15th Conf. on Automated Deduction (CADE), pp.286-300, 1998.
DOI : 10.1007/BFb0054266

C. Schürmann, Automating the meta theory of deductive systems, pp.0-146, 2000.