J. Aldrich, Resource-based programming in Plaid. Fun Ideas and Thoughts, 2010.

J. Aldrich, J. Sunshine, D. Saini, and Z. Sparks, Typestate-oriented programming, Proceeding of the 24th ACM SIGPLAN conference companion on Object oriented programming systems languages and applications, OOPSLA '09, pp.1015-1022, 2009.
DOI : 10.1145/1639950.1640073
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.150.2156

B. Aydemir, A. Bohannon, M. Fairbairn, J. Foster, B. Pierce et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, TPHOLs, number 3603 in LNCS, pp.50-65, 2005.
DOI : 10.1007/11541868_4

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

R. S. Bird and R. Paterson, de Bruijn notation as a nested datatype, Journal of Functional Programming, vol.9, issue.1, pp.77-91, 1999.
DOI : 10.1017/S0956796899003366

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, Why3: Shepherd your herd of provers, Boogie, pp.53-64, 2011.
URL : https://hal.archives-ouvertes.fr/hal-00790310

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

A. Chlipala, Parametric higher-order abstract syntax for mechanized semantics, ICFP, pp.143-156, 2008.

A. Chlipala, A verified compiler for an impure functional language, POPL, 2010.

N. G. De-bruijn, Lambda calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church- Rosser theorem, Proc. of the Koninklijke Nederlands Akademie, pp.380-392, 1972.

M. Fernández, I. Mackie, and F. Sinot, Lambda-Calculus with Director Strings, Applicable Algebra in Engineering, Communication and Computing, vol.11, issue.6, pp.393-437, 2005.
DOI : 10.1007/s00200-005-0169-9
URL : https://hal.archives-ouvertes.fr/inria-00133315

J. Filliâtre and A. Paskevich, Why3 ??? Where Programs Meet Provers, ESOP, pp.125-128, 2013.
DOI : 10.1007/978-3-642-37036-6_8

A. Flatau, A verified implementation of an applicative language with dynamic storage allocation, 1992.

M. J. Gabbay, Nominal Terms and Nominal Logics: From Foundations to Meta-mathematics, Handbook of Philosophical Logic, 2013.
DOI : 10.1007/978-94-007-6600-6_2

R. Hähnle, Tableaux and related methods, Handbook of Automated Reasoning, pp.100-178, 2001.

A. Hirschowitz and M. Maggesi, Nested Abstract Syntax in Coq, Journal of Automated Reasoning, vol.19, issue.3&4, pp.409-426, 2012.
DOI : 10.1007/s10817-010-9207-9
URL : https://hal.archives-ouvertes.fr/hal-01294214

G. Klein, J. Andronick, K. Elphinstone, G. Heiser, D. Cock et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.107-115, 2010.
DOI : 10.1145/1629575.1629596

R. Kumar, M. O. Myreen, S. Owens, and M. Norrish, CakeML, Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, 2014.
DOI : 10.1145/2535838.2535841

X. Leroy, A Formally Verified Compiler Back-end, Journal of Automated Reasoning, vol.27, issue.1, pp.363-446, 2009.
DOI : 10.1007/s10817-009-9155-4
URL : https://hal.archives-ouvertes.fr/inria-00360768

M. O. Myreen and M. J. Gordon, Verified LISP Implementations on ARM,??x86??and??PowerPC, TPHOLs, pp.359-374
DOI : 10.1007/978-3-540-71067-7_6

D. Oe, A. Stump, C. Oliver, and K. Clancy, versat: A Verified Modern SAT Solver, VMCAI, pp.363-378
DOI : 10.1016/j.scico.2007.07.008

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

F. Pottier, C?ml reference manual

N. Pouillard, Nameless, painless, ACM SIGPLAN Notices, vol.46, issue.9, pp.320-332, 2011.
DOI : 10.1145/2034574.2034817
URL : https://hal.archives-ouvertes.fr/hal-01110279

M. R. Shinwell, A. M. Pitts, and M. J. Gabbay, FreshML, ACM SIGPLAN Notices, vol.38, issue.9, pp.263-274, 2003.
DOI : 10.1145/944746.944729

A. Stump, M. Deters, A. Petcher, T. Schiller, and T. Simpson, Verified programming in Guru, Proceedings of the 3rd workshop on Programming languages meets program verification, PLPV '09, pp.49-58, 2009.
DOI : 10.1145/1481848.1481856