J. Andreoli, Logic Programming with Focusing Proofs in Linear Logic, Journal of Logic and Computation, vol.2, issue.3, pp.297-347, 1992.
DOI : 10.1093/logcom/2.3.297

D. Baelde, A. Gacek, D. Miller, G. Nadathur, and A. Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conference on Automated Deduction (CADE), F. Pfenning Number 4603 in LNAI, 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), pp.92-106, 2007.

S. Basu, M. Mukund, C. R. Ramakrishnan, I. V. Ramakrishnan, and R. M. Verma, Local and Symbolic Bisimulation Using Tabled Constraint Logic Programming, International Conference on Logic Programming (ICLP), pp.166-180, 2001.
DOI : 10.1007/3-540-45635-X_19

J. Bengtson and J. Parrow, Formalising the ??-Calculus Using Nominal Logic, Proceedings of FOSSACS 2007, pp.63-77, 2007.
DOI : 10.1007/978-3-540-71389-0_6

M. Boreale, Symbolic Trace Analysis of Cryptographic Protocols, Proceedings of ICALP 2001, pp.667-681, 2001.
DOI : 10.1007/3-540-48224-5_55

M. Boreale and R. D. Nicola, A Symbolic Semantics for the ??-calculus, Information and Computation, vol.126, issue.1, pp.34-52, 1996.
DOI : 10.1007/978-3-540-48654-1_24

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

N. G. De-bruijn, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem, Indag. Math, vol.34, issue.5, pp.381-392, 1972.

J. Despeyroux, A Higher-Order Specification of the ??-Calculus, Proc. of the IFIP International Conference on Theoretical Computer Science, IFIP TCS'2000, pp.425-439, 2000.
DOI : 10.1007/3-540-44929-9_30

L. Eriksson, A finitary version of the calculus of partial inductive definitions, Proceedings of the Second International Workshop on Extensions to Logic Programming, L.-H, 1991.
DOI : 10.1007/BFb0013605

M. J. Gabbay, The ??-Calculus in FM, Thirty-five years of, pp.80-149, 2003.
DOI : 10.1007/978-94-017-0253-9_10

M. J. Gabbay and A. M. Pitts, A New Approach to Abstract Syntax with Variable Binding, Formal Aspects of Computing, vol.13, issue.3-5, pp.341-363, 2001.
DOI : 10.1007/s001650200016

G. Gentzen, Investigations into logical deductions In The Collected Papers, pp.68-131, 1969.

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

L. Hallnäs and P. Schroeder-heister, A Proof-Theoretic Approach to Logic Programming, Journal of Logic and Computation, vol.1, issue.5, pp.635-660, 1991.
DOI : 10.1093/logcom/1.5.635

M. Hennessy and H. Lin, Symbolic bisimulations, Theoretical Computer Science, vol.138, issue.2, pp.353-389, 1995.
DOI : 10.1016/0304-3975(94)00172-F

D. Hirschkoff, A full formalization of pi-calculus theory in the Calculus of Constructions, International Conference on Theorem Proving in Higher Order Logics (TPHOLs'97 Number 1275 in LNCS. Murray Hill, pp.153-169, 1997.

F. Honsell, M. Lenisa, U. Montanari, and M. Pistore, Final semantics for the ??-calculus, Proc. of PROCOMET'98, 1998.
DOI : 10.1007/978-0-387-35358-6_17

F. Honsell, M. Miculan, and I. Scagnetto, ??-calculus in (Co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2001.
DOI : 10.1016/S0304-3975(00)00095-5

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

G. Huet and B. Lang, Proving and applying program transformations expressed with second-order patterns, Acta Informatica, vol.11, issue.1, pp.31-55, 1978.
DOI : 10.1007/BF00264598

C. Liang and D. Miller, Focusing and Polarization in Intuitionistic Logic, Computer Science Logic, J. LNCS, vol.4646, pp.451-465, 2007.
DOI : 10.1007/978-3-540-74915-8_34
URL : https://hal.archives-ouvertes.fr/inria-00167231

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

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

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

D. Miller, Abstract syntax for variable binders: An overview. In Computational Logic - CL, Number 1861 in LNAI, pp.239-253, 2000.

D. Miller and G. Nadathur, Some uses of higher-order logic in computational linguistics, Proceedings of the 24th annual meeting on Association for Computational Linguistics -, pp.247-255, 1986.
DOI : 10.3115/981131.981165

D. Miller and G. Nadathur, A logic programming approach to manipulating formulas and programs, IEEE Symposium on Logic Programming, S. Haridi, pp.379-388, 1987.

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 C. Palamidessi, Foundational aspects of syntax, ACM Computing Surveys, vol.31, issue.3es, 1999.
DOI : 10.1145/333580.333590

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

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, II, Information and Computation, vol.100, issue.1, pp.41-77, 1992.
DOI : 10.1016/0890-5401(92)90009-5

R. Milner, J. Parrow, and D. Walker, Modal logics for mobile processes, Theoretical Computer Science, vol.114, issue.1, pp.149-171, 1993.
DOI : 10.1016/0304-3975(93)90156-N

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

G. Nadathur, A treatment of higher-order features in logic programming, Theory and Practice of Logic Programming, vol.5, issue.03, pp.305-354, 2005.
DOI : 10.1017/S1471068404002297

G. Nadathur and N. Linnell, Practical Higher-Order Pattern Unification with On-the-Fly Raising, ICLP 2005: 21st International Logic Programming Conference, pp.371-386, 2005.
DOI : 10.1007/11562931_28

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 Conference on Automated Deduction (CADE), H. Ganzinger, Ed. Number 1632 in LNAI, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

T. Nipkow, Functional unification of higher-order patterns, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.64-74, 1993.
DOI : 10.1109/LICS.1993.287599

L. C. Paulson, Natural deduction as higher-order resolution, The Journal of Logic Programming, vol.3, issue.3, pp.237-258, 1986.
DOI : 10.1016/0743-1066(86)90015-4
URL : http://doi.org/10.1016/0743-1066(86)90015-4

L. C. Paulson, Isabelle: The next 700 theorem provers, Logic and Computer Science, pp.361-386, 1990.
DOI : 10.1007/BFb0030541

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 Conference on Automated Deduction Number 1632 in LNAI, pp.202-206, 1999.
DOI : 10.1007/3-540-48660-7_14

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

G. Plotkin, A structural approach to operational semantics. DAIMI FN-19, 1981.

D. Prawitz, Natural Deduction, 1965.

C. Röckl, D. Hirschkoff, and S. Berghofer, Higher-Order Abstract Syntax with Induction in Isabelle/HOL: Formalizing the ??-Calculus and Mechanizing the Theory of Contexts, 2001.
DOI : 10.1007/3-540-45315-6_24

D. Sangiorgi, A theory of bisimulation for the ??-calculus, Acta Informatica, vol.XVI, issue.2, pp.69-97, 1996.
DOI : 10.1007/s002360050036

D. Sangiorgi and D. Walker, ?-Calculus: A Theory of Mobile Processes, 2001.

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. F. Stärk, CUT-PROPERTY AND NEGATION AS FAILURE, International Journal of Foundations of Computer Science, vol.05, issue.02, pp.129-164, 1994.
DOI : 10.1142/S0129054194000086

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

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

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

A. Tiu, G. Nadathur, and D. Miller, Mixing finite success and finite failure in an automated prover, Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05, pp.79-98, 2005.

C. Urban and C. Tasson, Nominal techniques in Isabelle/HOL, 20th Conference on Automated Deduction (CADE), R. Nieuwenhuis, Ed. LNCS, pp.38-53, 2005.
DOI : 10.1007/s10817-008-9097-2
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.111.9675

A. Ziegler, D. Miller, and C. Palamidessi, A congruence format for name-passing calculi Electronic Notes in Theoretical Computer Science, Structural Operational Semantics (SOS'05), pp.169-189, 2005.