T. Altenkirch, A formalization of the strong normalization proof for System F in LEGO, Typed Lambda Calculi and Applications, 1993.
DOI : 10.1007/BFb0037095

T. Altenkirch and B. Reus, Monadic presentations of lambda terms using generalized inductive types. Pages 453?468 of: Computer Science Logic, Lecture Notes in Computer Science, vol.1683, 1999.

R. Atkey, Syntax for free: representing syntax with binding using parametricity. Pages 35?49 of: International Conference on Typed Lambda Calculi and Applications (TLCA), Lecture Notes in Computer Science, vol.5608, 2009.

R. Atkey, . Lindley, . Sam, and . Yallop, Unembedding domain-specific languages, Proceedings of the 2nd ACM SIGPLAN symposium on Haskell, Haskell '09, 2009.
DOI : 10.1145/1596638.1596644
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.167.4775

B. Aydemir, . Charguéraud, . Arthur, . Pierce, C. Benjamin et al., Engineering formal metatheory, Pages 3?15 of: ACM Symposium on Principles of Programming Languages (POPL), 2008.
DOI : 10.1145/1328438.1328443
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.103.5948

B. E. Aydemir, . Bohannon, . Aaron, . Fairbairn, . Matthew et al., Mechanized Metatheory for the Masses: The PoplMark Challenge, International Conference on Theorem Proving in Higher-Order Logics (TPHOLs). Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11541868_4

F. Bellegarde and J. Hook, Substitution: A formal methods case study using monads and transformations, Science of Computer Programming, vol.23, issue.2-3, pp.287-311, 1994.
DOI : 10.1016/0167-6423(94)00022-0

J. Bernardy, . Jansson, . Patrik, and R. Paterson, Parametricity and dependent types, Pages 345?356 of: Proceedings of the 15th ACM SIGPLAN international conference on Functional programming. ICFP '10, 2010.
DOI : 10.1145/1932681.1863592
URL : http://openaccess.city.ac.uk/13223/1/pts.pdf

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

A. Cave and . Pientka, Programming with binders and indexed data-types, Pages 413?424 of: ACM Symposium on Principles of Programming Languages (POPL), 2012.
DOI : 10.1145/2103656.2103705

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

C. Chen, . Xi, and . Hongwei, Implementing typeful program transformations, Pages 20?28 of: ACM Workshop on Evaluation and Semantics-Based Program Manipulation (PEPM), 2003.

J. Cheney, Scrap your nameplate, ACM International Conference on Functional Programming (ICFP), 2005.
DOI : 10.1145/1086365.1086389

A. Chlipala, A certified type-preserving compiler from lambda calculus to assembly language, Pages 54?65 of: ACM Conference on Programming Language Design and Implementation (PLDI), 2007.

N. Danielsson and . Anders, Agda standard library, 2011.

. De-bruijn and G. Nicolaas, Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem, Indag. Math, vol.34, issue.5, pp.381-392, 1972.

. De-bruijn and G. Nicolaas, Telescopic mappings in typed lambda calculus, Information and Computation, vol.91, issue.2, pp.189-204, 1991.
DOI : 10.1016/0890-5401(91)90066-B

K. Donnelly, . Xi, and . Hongwei, Combining higher-order abstract syntax with first-order abstract syntax in ATS, Proceedings of the 3rd ACM SIGPLAN workshop on Mechanized reasoning about languages with variable binding , MERLIN '05, 2005.
DOI : 10.1145/1088454.1088462

M. Fiore, . Plotkin, . Gordon, and D. Turi, Abstract syntax and variable binding (extended abstract) Pages 193?202 of, IEEE Symposium on Logic in Computer Science (LICS), 1999.

R. W. Floyd, Assigning meanings to programs. Pages 19?32 of: Mathematical Aspects of Computer Science, Proceedings of Symposia in Applied Mathematics, 1967.

L. Guillemette and S. Monnier, A type-preserving compiler in Haskell, ACM International Conference on Functional Programming (ICFP), 2008.

R. Harper, . Honsell, . Furio, and G. Plotkin, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.194-204, 1993.
DOI : 10.1145/138027.138060

C. A. Hoare, An axiomatic basis for computer programming, Communications of the ACM, vol.12, issue.10, pp.576-580, 1969.
DOI : 10.1145/363235.363259

G. Huet, The Zipper, Journal of Functional Programming, vol.7, issue.5, pp.549-554, 1997.
DOI : 10.1017/S0956796897002864

D. R. Licata and R. Harper, A universe of binding and computation, Pages 123?134 of: ACM International Conference on Functional Programming (ICFP), 2009.

C. Mcbride, The derivative of a regular type is its type of one-hole contexts, 2001.

C. Mcbride, First-order unification by structural recursion, Journal of Functional Programming, vol.13, issue.6, pp.1061-1075, 2003.
DOI : 10.1017/S0956796803004957

C. Mcbride and J. Mckinna, The view from the left, Journal of Functional Programming, vol.14, issue.1, pp.69-111, 2004.
DOI : 10.1017/S0956796803004829

C. Mcbride and R. Paterson, Applicative programming with effects, Journal of Functional Programming, vol.18, issue.01, pp.1-13, 2008.
DOI : 10.1017/S0956796800003658

J. C. Mitchell, Representation independence and data abstraction, Proceedings of the 13th ACM SIGACT-SIGPLAN symposium on Principles of programming languages , POPL '86, 1986.
DOI : 10.1145/512644.512669

U. Norell, Towards a practical programming language based on dependent type theory, pp.412-96, 2007.

F. Pfenning, . Lee, and . Peter, LEAP: A language with eval and polymorphism, Pages 345?359 of: International Joint Conference on Theory and Practice of Software Development (TAPSOFT). Lecture Notes in Computer Science, 1989.
DOI : 10.1007/3-540-50940-2_46

B. Pientka, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, Pages 371?382 of: ACM Symposium on Principles of Programming Languages (POPL), 2008.

A. M. Pitts, Alpha-structural recursion and induction, Journal of the ACM, vol.53, issue.3, pp.459-506, 2006.
DOI : 10.1145/1147954.1147961
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.85.518

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

A. Poswolsky and C. Schürmann, Practical Programming with Higher-Order Encodings and Dependent Types, Pages 93?107 of: European Symposium on Programming (ESOP). Lecture Notes in Computer Science, 2008.
DOI : 10.1007/978-3-540-78739-6_7
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.107.2605

A. Poswolsky and C. Schürmann, System Description: Delphin ??? A Functional Programming Language for Deductive Systems, Electronic Notes in Theoretical Computer Science, vol.228, pp.113-120, 2009.
DOI : 10.1016/j.entcs.2008.12.120

F. Pottier, An overview of C?ml. Pages 27?52 of, ACM Workshop on ML. Electronic Notes in Theoretical Computer Science, vol.148, issue.2, 2006.

F. Pottier, Static Name Control for FreshML, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), 2007.
DOI : 10.1109/LICS.2007.44

N. Pouillard, Nameless, painless, Proceedings of the 16th ACM SIGPLAN international conference on Functional programming. ICFP '11, 2011.
DOI : 10.1145/2034773.2034817
URL : https://hal.archives-ouvertes.fr/hal-01110279

N. Pouillard, Nompa (Agda code), 2011.

N. Pouillard, A unifying approach to safe programming with first-order syntax with binders, 2012.
URL : https://hal.archives-ouvertes.fr/tel-00759059

N. Pouillard, . Pottier, and . François, A fresh look at programming with names and binders. Pages 217?228 of, Proceedings of the 15th ACM SIGPLAN international conference on Functional programming. ICFP '10, 2010.

J. C. Reynolds, Types, abstraction and parametric polymorphism. Pages 513?523 of: Information Processing 83, 1983.

M. Sato and R. Pollack, External and internal syntax of the <mml:math altimg="si1.gif" display="inline" overflow="scroll" xmlns:xocs="http://www.elsevier.com/xml/xocs/dtd" xmlns:xs="http://www.w3.org/2001/XMLSchema" xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance" xmlns="http://www.elsevier.com/xml/ja/dtd" xmlns:ja="http://www.elsevier.com/xml/ja/dtd" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:tb="http://www.elsevier.com/xml/common/table/dtd" xmlns:sb="http://www.elsevier.com/xml/common/struct-bib/dtd" xmlns:ce="http://www.elsevier.com/xml/common/dtd" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:cals="http://www.elsevier.com/xml/common/cals/dtd"><mml:mi>??</mml:mi></mml:math>-calculus, Journal of Symbolic Computation, vol.45, issue.5, pp.598-616, 2010.
DOI : 10.1016/j.jsc.2010.01.010

C. Schürmann, . Poswolsky, . Adam, and J. Sarnat, The $\nabla$ -Calculus. Functional Programming with Higher-Order Encodings, Pages 339?353 of: International Conference on Typed Lambda Calculi and Applications (TLCA). Lecture Notes in Computer Science, 2005.
DOI : 10.1007/11417170_25

M. R. Shinwell, A. M. Pitts, . Gabbay, and J. Murdoch, FreshML: Programming with binders made simple, Pages 263?274 of: ACM International Conference on Functional Programming (ICFP), 2003.

I. Stark, Names and higher-order functions, 1994.

P. Wadler, Theorems for free! Pages 347?359 of: Conference on Functional Programming Languages and Computer Architecture (FPCA), 1989.

S. Weirich, . Yorgey, . Brent, and T. Sheard, Binders unbound, Proceedings of the 16th ACM SIGPLAN international conference on Functional programming. ICFP '11, 2011.