F. Arnon-avron, I. A. Honsell, R. Mason, and . Pollack, Using Typed Lambda Calculus to Implement Formal Systems on a Machine, Journal of Automated Reasoning, vol.9, pp.309-354, 1992.

B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce et al., Mechanized Metatheory for the Masses: The POPLmark Challenge, Theorem Proving in Higher Order Logics: 18th International Conference (LNCS), pp.50-65, 2005.

D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur et al., Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, pp.1-89, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

A. Charguéraud, The Locally Nameless Representation, Journal of Automated Reasoning, pp.1-46, 2011.

J. Cheney and C. Urban, Alpha-Prolog: A Logic Programming Language with Names, Binding, and Alpha-Equivalence, Logic Programming, 20th International Conference, vol.3132, pp.269-283, 2004.

S. K. Anthony, P. J. Cheng, J. Robinson, and . Staples, Higher Level Meta Programming in Qu-Prolog 3: 0, Logic Programming, Proceedings of the Eigth International Conference, pp.285-298, 1991.

J. Chirimar, Proof Theoretic Approach to Specification Languages, Ph.D. Dissertation. University of Pennsylvania, 1995.

A. Chlipala, Parametric higher-order abstract syntax for mechanized semantics, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.143-156, 2008.

A. Church, A Formulation of the Simple Theory of Types, J. of Symbolic Logic, vol.5, pp.56-68, 1940.

N. Govert-de-bruijn, Lambda Calculus Notation with Nameless Dummies, a Tool for Automatic Formula Manipulation, with an Application to the Church-Rosser Theorem, Indagationes Mathematicae, vol.34, pp.381-392, 1972.

J. Despeyroux, A. Felty, and A. Hirschowitz, Higher-order abstract syntax in Coq, Second International Conference on Typed Lambda Calculi and Applications, pp.124-138, 1995.
URL : https://hal.archives-ouvertes.fr/inria-00074124

C. Dunchev, F. Guidi, C. Sacerdoti-coen, and E. Tassi, ELPI: Fast, Embeddable, ?Prolog Interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference, vol.9450, pp.460-468, 2015.

A. P. Felty, A. Momigliano, and B. Pientka, The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 2-A Survey, J. of Automated Reasoning, vol.55, pp.307-372, 2015.

F. Ferreira and B. Pientka, Programs Using Syntax with First-Class Binders, Proceedings of the 26th European Symposium on Programming, vol.10201, pp.504-529, 2017.

M. J. Gabbay and A. M. Pitts, A new approach to abstract syntax involving binders, 14th Symp. on Logic in Computer Science, pp.214-224, 1999.

A. Gacek, A Framework for Specifying, Prototyping, and Reasoning about Computational Systems, 2009.

A. Gacek, D. Miller, and G. Nadathur, Combining generic judgments with recursive definitions, 23th Symp. on Logic in Computer Science, F. Pfenning, pp.33-44, 2008.

A. Gacek, D. Miller, and G. Nadathur, Nominal abstraction, Information and Computation, vol.209, pp.48-73, 2011.

U. Gérard, Computing with relations, functions, and bindings, 2019.

U. Gérard, D. Miller, and G. Scherer, Try MLTS Online, 2018.

A. Gordon, A Mechanisation of Name-Carrying Syntax up to Alpha-Conversion, International Workshop on Higher Order Logic Theorem Proving and its Applications, vol.780, pp.414-426, 1994.

M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol.78, 1979.

J. C. Michael and . Gordon, Introduction to the HOL System, Proceedings of the International Workshop on the HOL Theorem Proving System and its Applications, pp.2-3, 1991.

R. Harper, F. Honsell, and G. Plotkin, A Framework for Defining Logics, J. ACM, vol.40, pp.143-184, 1993.

J. Harrison, HOL Light: an overview, International Conference on Theorem Proving in Higher Order Logics, pp.60-66, 2009.

G. Huet, A Unification Algorithm for Typed ?-Calculus, Theoretical Computer Science, vol.1, pp.27-57, 1975.

G. Kahn, Natural Semantics, Proceedings of the Symposium on Theoretical Aspects of Computer Science (LNCS), vol.247, pp.22-39, 1987.
URL : https://hal.archives-ouvertes.fr/inria-00075953

R. Daniel, R. Licata, and . Harper, A Universe of Binding and Computation, Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming (ICFP '09), pp.123-134, 2009.

C. Mcbride and J. Mckinna, Functional pearl: I am not a number -I am a free variable, Proceedings of the ACM SIGPLAN Workshop on Haskell, 2004.

, , pp.1-9

D. Miller, An Extension to ML to Handle Bound Variables in Data Structures: Preliminary Report, Proceedings of the Logical Frameworks BRA Workshop, pp.323-335, 1990.

D. Miller, A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, J. of Logic and Computation, vol.1, pp.497-536, 1991.

D. Miller, Unification under a mixed prefix, Journal of Symbolic Computation, vol.14, p.90011, 1992.

D. Miller, Forum: A Multiple-Conclusion Specification Logic, Theoretical Computer Science, vol.165, issue.96, p.45, 1996.

D. Miller, Bindings, mobility of bindings, and the ?-quantifier, 18th International Conference on Computer Science Logic (CSL) 2004 (LNCS), vol.3210, 2004.

D. Miller, Mechanized Metatheory Revisited, Journal of Automated Reasoning, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01884210

D. Miller and G. Nadathur, Programming with Higher-Order Logic, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776197

D. Miller and C. Palamidessi, Foundational Aspects of Syntax. Comput. Surveys, vol.31, 1999.

D. Miller and A. Tiu, A proof theory for generic judgments, ACM Trans. on Computational Logic, vol.6, pp.749-783, 2005.

G. Nadathur and D. Miller, An Overview of ?Prolog, Fifth International Logic Programming Conference, pp.810-827, 1988.

T. Nipkow, Functional Unification of Higher-Order Patterns, 8th Symp. on Logic in Computer Science, pp.64-74, 1993.

. Ocaml, , 2018.

L. C. Paulson, The Foundation of a Generic Theorem Prover, Journal of Automated Reasoning, vol.5, pp.363-397, 1989.

C. Lawrence and . Paulson, Isabelle: A Generic Theorem Prover, Number 828 in LNCS, 1994.

F. Pfenning and C. Elliott, Higher-Order Abstract Syntax, Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp.199-208, 1988.

F. Pfenning and C. Schürmann, System Description: Twelf -A Meta-Logical Framework for Deductive Systems, 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger, pp.202-206, 1999.

B. Pientka and J. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010.

A. M. Pitts, Nominal Logic, A First Order Theory of Names and Binding, Information and Computation, vol.186, pp.165-193, 2003.

A. M. Pitts and M. J. Gabbay, A Metalanguage for Programming with Bound Names Modulo Renaming, Mathematics of Program Construction. 5th International Conference, vol.1837, pp.230-255, 2000.

A. Poswolsky and C. Schürmann, Practical programming with higher-order encodings and dependent types, Proceedings of the European Symposium on Programming, 2008.

A. Poswolsky and C. Schürmann, System Description: Delphin -A Functional Programming Language for Deductive Systems, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, vol.228, pp.113-120, 2008.

F. Pottier, An Overview of C? ml, Proceedings of the ACM-SIGPLAN Workshop on ML (ML 2005) (Electr. Notes Theor, vol.148, pp.27-52, 2006.

F. Pottier, Static name control for FreshML, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS, pp.356-365, 2007.

X. Qi, A. Gacek, S. Holte, G. Nadathur, and Z. Snow, The Teyjus System -Version 2, 2015.

D. Sangiorgi, ? -calculus, internal mobility and agent-passing calculi, Theoretical Computer Science, vol.167, pp.235-274, 1996.

C. Schürmann, A. Poswolsky, and J. Sarnat, The nablacalculus. Functional Programming with Higher-order Encodings, Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications (TLCA'05, 2005.

, The Seventeen Provers of the World (LNCS), Freek Wiedijk, vol.3600, pp.151-157

D. Scott, Outline of a Mathematical Theory of Computation, Proceedings, Fourth Annual Princeton Conference on Information Sciences and Systems. Princeton University, pp.169-176, 1970.

M. R. Shinwell, A. M. Pitts, and M. J. Gabbay, FreshML: Programming with Binders Made Simple, Eighth ACM SIGPLAN International Conference on Functional Programming, pp.263-274, 2003.

Y. Wang, K. Chaudhuri, A. Gacek, and G. Nadathur, Reasoning about Higher-Order Relational Specifications, Proceedings of the 15th International Symposium on Princples and Practice of Declarative Programming, pp.157-168, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00787126