D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

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), number 4603 in Lecture Notes in Artificial Intelligence, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

J. Bengtson and J. Parrow, Formalising the ??-Calculus Using Nominal Logic, Logical Methods in Computer Science, vol.5, issue.2, pp.1-36, 2009.
DOI : 10.1007/978-3-540-71389-0_6

F. Bonchi and D. Pous, Checking NFA equivalence with bisimulations up to congruence, ACM SIGPLAN- SIGACT Symposium on Principles of Programming Languages (POPL), pp.457-468, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00639716

K. Chaudhuri, M. Cimini, and D. Miller, The Abella formalization of bisimulation-up-to for CCS and the ?-calculus. Available from http

J. Endrullis, D. Hendriks, and M. Bodin, Circular Coinduction in Coq Using Bisimulation-Up-To Techniques, Lecture Notes in Computer Science, vol.7998, pp.354-369, 2013.
DOI : 10.1007/978-3-642-39634-2_26

M. J. Gabbay, The ??-Calculus in FM, Thirty Five Years of Automating Mathematics of Applied Logic Series, pp.80-149, 2004.
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

A. Gacek, A Framework for Specifying, Prototyping, and Reasoning about Computational Systems, 2009.

A. Gacek, D. Miller, and G. , Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004

G. Gentzen, New version of the consistency proof for elementary number theory, pp.252-286, 1938.

F. Honsell and M. , Miculan, and I. Scagnetto. ?-calculus in (co)inductive type theories, Theoretical Computer Science, vol.2, issue.253, pp.239-285, 2001.

C. Hur, G. Neis, D. Dreyer, and V. Vafeiadis, The power of parameterization in coinductive proof, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.193-206, 2013.

J. Madiot, D. Pous, and D. Sangiorgi, Bisimulations Up-to: Beyond First-Order Transition Systems, Proceedings of the 25th International Conference on Concurrency Theory (CONCUR), pp.93-108, 2014.
DOI : 10.1007/978-3-662-44584-6_8
URL : https://hal.archives-ouvertes.fr/hal-00990859

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

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, Communication and Concurrency, 1989.

D. Pous, Weak Bisimulation Up to Elaboration, Lecture Notes in Computer Science, vol.4137, pp.390-405, 2006.
DOI : 10.1007/11817949_26
URL : https://hal.archives-ouvertes.fr/hal-01441462

D. Pous, Complete Lattices and Up-To Techniques, Lecture Notes in Computer Science, vol.4807, pp.351-366, 2007.
DOI : 10.1007/978-3-540-76637-7_24
URL : https://hal.archives-ouvertes.fr/ensl-00155308

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method, Advanced Topics in Bisimulation and Coinduction, pp.233-289, 2011.
DOI : 10.1017/CBO9780511792588.007
URL : https://hal.archives-ouvertes.fr/hal-00909391

D. Sangiorgi, On the bisimulation proof method, Mathematical Structures in Computer Science, vol.8, issue.5, pp.447-479, 1998.
DOI : 10.1017/S0960129598002527

D. Sangiorgi and R. Milner, The problem of ???weak bisimulation up to???, In CONCUR Lecture Notes in Computer Science, vol.630, pp.32-46, 1992.
DOI : 10.1007/BFb0084781

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

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