S. Ambler and R. L. Crole, Mechanized Operational Semantics via (Co)Induction, TPHOLs'99, pp.221-238, 1999.
DOI : 10.1007/3-540-48256-3_15
URL : http://www.mcs.le.ac.uk/~sambler/papers/mosci98.ps.gz

A. Anand and V. Rahli, Towards a Formally Verified Proof Assistant, ITP 2014, pp.27-44, 2014.
DOI : 10.1007/978-3-319-08970-6_3

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

S. Richard, R. Bird, and . Paterson, De Bruijn Notation as a Nested Datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999.

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012.
DOI : 10.1007/s10817-008-9097-2

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

S. Dal and Z. , Mobile Processes: a Commented Bibliography, MOVEP'2K ? 4th Summer school on Modelling and Verification of Parallel processes, pp.206-222, 2001.
URL : https://hal.archives-ouvertes.fr/hal-01483577

E. De, V. , and V. Koutavas, Locally Nameless Permutation Types, 2012.

S. J. Gay, A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL, pp.217-232, 2001.
DOI : 10.1007/3-540-44755-5_16

A. D. Gordon, Bisimilarity as a Theory of Functional Programming, Electronic Notes in Theoretical Computer Science, vol.1, pp.232-252, 1995.
DOI : 10.1016/S1571-0661(04)80013-6

D. Hirschkoff and D. Pous, A Distribution Law for CCS and a New Congruence Result for the ??-Calculus, Lecture Notes in Computer Science), vol.4423, pp.228-242, 2007.
DOI : 10.1007/978-3-540-71389-0_17
URL : https://hal.archives-ouvertes.fr/hal-00089219

D. J. Howe, Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, vol.124, issue.2, pp.103-112, 1996.
DOI : 10.1006/inco.1996.0008

S. Lenglet and A. Schmitt, Howe's Method for Contextual Semantics, 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs) Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.212-225, 2015.

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

P. Maksimovic and A. Schmitt, HOCore in Coq, ITP 2015, pp.278-293, 2015.
DOI : 10.1007/978-3-319-22102-1_19
URL : https://hal.archives-ouvertes.fr/hal-01243017

A. Momigliano, A supposedly fun thing i may have to do again, Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice, LFMTP '12, pp.33-42, 2012.
DOI : 10.1145/2364406.2364411

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

R. Perera and J. Cheney, Proof-relevant ??-calculus: a constructive account of concurrency and causality, Mathematical Structures in Computer Science, vol.10, 2016.
DOI : 10.1016/0304-3975(89)90050-9

F. Pfenning and C. Elliott, Higher-Order Abstract Syntax, PLDI 88, pp.199-208, 1988.

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

D. Sangiorgi, Bisimulation for Higher-Order Process Calculi, Information and Computation, vol.131, issue.2, pp.141-178, 1996.
DOI : 10.1006/inco.1996.0096
URL : https://hal.archives-ouvertes.fr/inria-00074170

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

D. Thibodeau, A. Momigliano, and B. Pientka, A Case-Study in Programming Coinductive Proofs: Howe's Method, 2016.