J. Bengtson and J. Parrow, Psi-calculi in isabelle, Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pp.99-114, 2009.

S. Boulier and A. Schmitt, Formalisation de hocore en coq, Actes des 23èmes Journées Francophones des Langages Applicatifs, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00665945

T. Braibant and D. Pous, Deciding Kleene Algebras in Coq, Logical Methods in Computer Science, vol.8, issue.1, pp.1-42, 2012.
DOI : 10.2168/LMCS-8(1:16)2012
URL : https://hal.archives-ouvertes.fr/hal-00383070

Z. Cao, More on bisimulations for higher order pi-calculus, Proc. of FoSSaCS'06, pp.63-78, 2006.

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.1-46, 2011.
DOI : 10.1007/s10817-011-9225-2

E. Gimenez, A Tutorial on Recursive Types in Coq, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00069950

G. Gonthier, A computer-checked proof of the four colour theorem Available on-line at, 2004.

D. Hirschkoff, A full formalisation of pi-calculus theory in the calculus of constructions, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, pp.153-169, 1997.

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

B. Huffman and C. Urban, A New Foundation for Nominal Isabelle, Interactive Theorem Proving, First International Conference Proceedings, pp.35-50, 2010.
DOI : 10.1007/978-3-642-14052-5_5

A. Jeffrey and J. Rathke, Contextual equivalence for higher-order pi-calculus revisited, Logical Methods in Computer Science, vol.1, issue.1, pp.1-22, 2005.
DOI : 10.2168/LMCS-1(1:4)2005

I. Lanese, J. A. Pérez, D. Sangiorgi, and A. Schmitt, On the expressiveness and decidability of higher-order process calculi, Information and Computation, vol.209, issue.2, pp.198-226, 2011.
DOI : 10.1016/j.ic.2010.10.001
URL : https://hal.archives-ouvertes.fr/inria-00494584

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

R. Milner and F. Moller, Unique decomposition of processes, Theoretical Computer Science, vol.107, issue.2, pp.357-363, 1993.
DOI : 10.1016/0304-3975(93)90176-T

J. Parrow, J. Borgström, P. Raabjerg, and J. Å. Pohjola, Higher-order psi-calculi, Mathematical Structures in Computer Science, vol.13, pp.1-37
DOI : 10.1016/S0304-3975(00)00097-9

R. Pollack, M. Sato, and W. Ricciotti, A Canonical Locally Named Representation of Binding, Journal of Automated Reasoning, vol.40, issue.4, pp.1-23, 1007.
DOI : 10.1007/s10817-011-9229-y

N. Pouillard and F. Pottier, A fresh look at programming with names and binders, Proceedings of the fifteenth ACM SIGPLAN International Conference on Functional Programming, pp.217-228, 2010.

D. Sangiorgi, Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms, 1992.

D. Sangiorgi, Bisimulation for higher-order process calculi. Information and Computation, pp.141-178, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00074170

D. Sangiorgi, ??-Calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, vol.167, issue.1-2, pp.235-274, 1996.
DOI : 10.1016/0304-3975(96)00075-8

B. Thomsen, A calculus of higher order communicating systems, Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages , POPL '89, pp.143-154, 1989.
DOI : 10.1145/75277.75290

B. Thomsen, Calculi for Higher Order Communicating Systems, 1990.

B. Thomsen, Plain CHOCS A second generation calculus for higher order processes, Acta Informatica, vol.5, issue.2, pp.1-59, 1993.
DOI : 10.1007/BF01200262

A. Tiu and D. Miller, Proof search specifications of bisimulation and modal logics for the picalculus, ACM Transactions on Computational Logic (TOCL), vol.1113, pp.1-1335, 2010.

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

C. Urban, J. Cheney, and S. Berghofer, Mechanizing the metatheory of LF, ACM Trans. Comput. Log, vol.12, issue.2, p.15, 2011.

C. Urban and C. Kaliszyk, General bindings and alpha-equivalence in nominal isabelle, Programming Languages and Systems -20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software. Proceedings, pp.480-500, 2011.