S. Ambler and R. L. Crole, Mechanized operational semantics via (co)induction, TPHOLs'99, vol.1690, pp.221-238, 1999.

A. Anand and V. Rahli, Towards a formally verified proof assistant, Lecture Notes in Computer Science, vol.8558, pp.27-44, 2014.

B. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce et al., Mechanized metatheory for the masses: The PoplMark challenge, TPHOLs, pp.50-65, 2005.

B. E. Aydemir and S. Weirich, LNgen: Tool support for locally nameless representations, 2010.

D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A system for reasoning about relational specifications, J. Formalized Reasoning, vol.7, issue.2, pp.1-89, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

J. Bengtson and J. Parrow, Formalising the pi-calculus using nominal logic, Logical Methods in Computer Science, vol.5, issue.2, 2009.

R. S. Bird and R. Paterson, De Bruijn notation as a nested datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999.

A. Bucalo, F. Honsell, M. Miculan, I. Scagnetto, and M. Hofmann, Consistency of the theory of contexts, J. Funct. Program, vol.16, issue.3, pp.327-372, 2006.

I. Cervesato and F. Pfenning, A linear logical framework, Inf. Comput, vol.179, issue.1, pp.19-75, 2002.

I. Cervesato, F. Pfenning, D. Walker, and K. Watkins, A concurrent logical framework ii: Examples and applications, 2002.

A. Charguéraud, LN:locally nameless representation with cofinite quantification

A. Charguéraud, TLC: A non-constructive library for Coq

A. Charguéraud, The locally nameless representation, Journal of Automated Reasoning, vol.49, issue.3, pp.363-408, 2012.

A. Ciaffaglione and I. Scagnetto, Mechanizing type environments in weak, HOAS. Theor. Comput. Sci, vol.606, pp.57-78, 2015.

S. Dal-zilio, Mobile Processes: a Commented Bibliography. In MOVEP'2K -4th Summer school on Modelling and Verification of Parallel processes, Lecture Notes in Computer Science, vol.2067, pp.206-222, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01483577

N. Govert-de-bruijn, Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes Mathematicae, vol.75, issue.5, pp.381-392, 1972.

J. Despeyroux, A higher-order specification of the pi-calculus, Lecture Notes in Computer Science, vol.1872, pp.425-439, 2000.

J. Despeyroux, A. P. Felty, and A. Hirschowitz, Higher-order abstract syntax in coq, TLCA '95, vol.902, pp.124-138, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00074124

S. J. Gay, A framework for the formalisation of pi calculus type systems in Isabelle/HOL, vol.2152, pp.217-232, 2001.

A. D. Gordon, Bisimilarity as a theory of functional programming, Electronic Notes in Theoretical Computer Science, vol.1, pp.232-252, 1995.

L. Henry-gréard, Proof of the subject reduction property for a pi-calculus in COQ, INRIA, 1999.

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, vol.1275, pp.153-169, 1997.

D. Hirschkoff, Up to context proofs for the ?-calculus in the Coq system, 1997.

D. Hirschkoff and D. Pous, A distribution law for CCS and a new congruence result for the pi-calculus, Proc. of FoSSaCS'07, vol.4423, pp.228-242
URL : https://hal.archives-ouvertes.fr/hal-00089219

. Springer, , 2007.

F. Honsell, I. Marino-miculan, and . Scagnetto, pi-calculus in (co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2000.

F. Honsell, I. Marino-miculan, and . Scagnetto, The theory of contexts for first order and higher order abstract syntax, Electr. Notes Theor. Comput. Sci, vol.62, pp.116-135, 2001.

D. J. Howe, Proving congruence of bisimulation in functional programming languages. Information and Computation, vol.124, pp.103-112, 1996.

M. J. Gabbay, The pi-calculus in fm, Thirty Five Years of Automating Mathematics, vol.28, pp.247-269, 2003.

S. Keuchel, S. Weirich, and T. Schrijvers, Needle & knot: Binder boilerplate tied up, ESOP 16, vol.9632, pp.419-445

. Springer, , 2016.

S. Lenglet and A. Schmitt, Howe's method for contextual semantics, 26th International Conference on Concurrency Theory, vol.42, pp.212-225, 2015.

S. Lenglet and A. Schmitt, HO? in Coq, pp.252-265, 2018.

S. Lenglet, A. Schmitt, and J. Stefani, Characterizing contextual equivalence in calculi with passivation. Information and Computation, vol.209, pp.1390-1433, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00903877

P. Maksimovic and A. Schmitt, Hocore in Coq, Lecture Notes in Computer Science, vol.9236, pp.278-293, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01243017

J. Mckinna and R. Pollack, Pure type systems formalized, TLCA '93, vol.664, pp.289-305, 1993.

T. F. Melham, A mechanized theory of the pi-calculus in HOL, Nord. J. Comput, vol.1, issue.1, pp.50-76, 1994.

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Trans. Comput. Log, vol.6, issue.4, pp.749-783, 2005.

R. Milner, J. Parrow, and D. Walker, A calculus of mobile processes, i. Information and Computation, vol.100, pp.1-40, 1992.

M. Otmane-aït, Mechanizing a pi-calculus equivalence in hol, TPHOL 95, pp.1-16, 1995.

A. Momigliano, A supposedly fun thing I may have to do again: a HOAS encoding of Howe's method, LFMTP 12, pp.33-42, 2012.

J. Parrow, J. Borgström, P. Raabjerg, and J. Pohjola, Higher-order psi-calculi, Mathematical Structures in Computer Science, vol.3, pp.1-37, 2014.

R. Perera and J. Cheney, Proof-relevant ?-calculus: a constructive account of concurrency and causality, Mathematical Structures in Computer Science, vol.28, issue.9, pp.1541-1577, 2018.

F. Pfenning and C. Elliott, Higher-order abstract syntax, PLDI 88, pp.199-208, 1988.

F. Pfenning and C. Schürmann, System description: Twelf -A meta-logical framework for deductive systems, Lecture Notes in Computer Science, vol.99, pp.202-206, 1999.

B. Pientka and J. Dunfield, Beluga: A framework for programming and reasoning with deductive systems (system description), IJCAR 2010, vol.6173, pp.15-21, 2010.

A. M. Pitts, Nominal logic, a first order theory of names and binding, Inf. Comput, vol.186, issue.2, pp.165-193, 2003.

C. Röckl, A first-order syntax for the pi-calculus in isabelle/hol using permutations, Electr. Notes Theor. Comput. Sci, vol.58, issue.1, pp.1-17, 2001.

C. Röckl and D. Hirschkoff, A fully adequate shallow embedding of the [pi]-calculus in isabelle/hol with mechanized syntax analysis, J. Funct. Program, vol.13, issue.2, pp.415-451, 2003.

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

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

K. Stark, S. Schäfer, and J. Kaiser, Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions, CPP, vol.19, pp.166-180, 2019.

T. Penn and P. L. Club, The Penn locally nameless metatheory library

D. Thibodeau, A. Momigliano, and B. Pientka, A case-study in programming coinductive proofs: Howe's method. available at momigliano.di.unimi.it/papers/ bhowe.pdf, 2016.

C. Urban, Nominal techniques in Isabelle/HOL, J. Autom. Reasoning, vol.40, issue.4, pp.327-356, 2008.

C. Urban, S. Berghofer, and C. Kaliszyk, Nominal 2. Archive of Formal Proofs, 2013.