, The Abella Prover Available at http://abella-prover.org, 2012.

D. Baelde and K. Chaudhuri, Abella: A System for Reasoning about Relational Specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709

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

W. F. and C. Mellish, Programming in Prolog, 1987.

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.
DOI : 10.1007/BFb0014049
URL : https://hal.archives-ouvertes.fr/inria-00074124

A. Gacek, D. Miller-&-gopalan, and . Nadathur, Nominal abstraction, Information and Computation, vol.209, issue.1, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004

U. Gérard and &. Miller, Separating Functional Computation from Relations, Valentin Goranko & Mads Dam 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), LIPIcs 82, pp.1-23, 2017.

U. Gérard and &. Miller, Functional programming with ? -tree syntax: Draft. Available from https, 2018.

U. Gérard and &. Miller, TryMLTS. https://trymlts.github.io, 2018.

M. Hofmann, Semantical analysis of higher-order abstract syntax, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.204-213, 1999.
DOI : 10.1109/LICS.1999.782616

P. J. Landin, The Mechanical Evaluation of Expressions, The Computer Journal, vol.6, issue.4, pp.308-320, 1964.
DOI : 10.1093/comjnl/6.4.308

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, Journal of Logic and Computation, vol.1, issue.4, pp.497-536, 1991.
DOI : 10.1093/logcom/1.4.497

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

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

A. Nanevski, F. Pfenning-&-brigitte, and . Pientka, Contextual modal type theory, ACM Transactions on Computational Logic, vol.9, issue.3, pp.1-49, 2008.
DOI : 10.1145/1352582.1352591

B. Nordstrom, K. Petersson, &. Jan, and M. Smith, Programming in Martin-Löf's type theory : an introduction, International Series of Monographs on Computer Science, 1990.

, OCaml, 2018.

B. Pientka and &. Dunfield, Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), Fifth International Joint Conference on Automated Reasoning, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2