B. Aydemir, A. Bohannon, and S. Weirich, Nominal Reasoning Techniques in Coq, International Workshop on Logical Frameworks and Meta-Languages:Theory and Practice (LFMTP), pp.69-77, 2006.
DOI : 10.1016/j.entcs.2007.01.028

S. A. Aydemir, S. Zdancewic, and . Weirich, Abstracting syntax, 2009.

E. Brian, A. Aydemir, M. Bohannon, J. N. Fairbairn, B. C. Foster et al., Mechanized metatheory for the masses: The POPLmark challenge, Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in LNCS, pp.50-65, 2005.

E. Brian, A. Aydemir, S. Bohannon, and . Weirich, Nominal reasoning techniques in Coq: (extended abstract), Electr. Notes Theor. Comput. Sci, vol.174, issue.5, pp.69-77, 2007.

. Baelde, Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012.

K. Baelde, A. Chaudhuri, D. Gacek, G. Miller, A. Nadathur et al., Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, p.2014
URL : https://hal.archives-ouvertes.fr/hal-01102709

A. Baelde, D. Gacek, G. Miller, A. Nadathur, and . Tiu, The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pp.391-397, 2007.
DOI : 10.1007/978-3-540-73595-3_28

U. Berger, S. Berghofer, P. Letouzey, and H. Schwichtenberg, Program Extraction from Normalization Proofs, Studia Logica, vol.11, issue.1, pp.25-49, 2006.
DOI : 10.1007/s11225-006-6604-5
URL : https://hal.archives-ouvertes.fr/hal-00150904

F. Bonchi and D. Pous, Checking NFA equivalence with bisimulations up to congruence, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pp.457-468, 2013.
URL : https://hal.archives-ouvertes.fr/hal-00639716

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

M. 13-kaustuv-chaudhuri, D. Cimini, and . Miller, A lightweight formalization of the metatheory of bisimulation-up-to, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pp.157-166, 2015.

J. Cheney and C. Urban, Nominal logic programming, ACM Transactions on Programming Languages and Systems, vol.30, issue.5, pp.1-47, 2008.
DOI : 10.1145/1387673.1387675
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.342.6780

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, The Journal of Symbolic Logic, vol.1, issue.02, pp.56-68, 1940.
DOI : 10.2307/2371199

D. Clément, J. Despeyroux, T. Despeyroux, L. Hascoët, and G. Kahn, Natural semantics on the computer, Research Report, vol.416, 1985.

R. L. Constable, Implementing Mathematics with the Nuprl Proof Development System, 1986.

T. Coquand and G. Huet, The calculus of constructions, Information and Computation, vol.76, issue.2-3, pp.95-120, 1988.
DOI : 10.1016/0890-5401(88)90005-3
URL : https://hal.archives-ouvertes.fr/inria-00076024

G. De-bruijn, A Survey of the Project Automath, To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus, and Formalism, pp.589-606, 1980.
DOI : 10.1016/S0049-237X(08)70203-9

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

C. 23-cvetan-dunchev, E. Sacerdoti-coen, and . Tassi, Implementing HOL in an higher order logic programming language, Proceedings of the Eleventh Workshop on Logical Frameworks and Meta- Languages: Theory and Practice, pp.1-410, 2016.

F. 24-cvetan-dunchev, C. Guidi, E. Sacerdoti-coen, and . Tassi, ELPI: fast, embeddable, ?Prolog interpreter, Logic for Programming, Artificial Intelligence, and Reasoning -20th International Conference Proceedings, pp.460-468, 2015.

A. Felty and D. Miller, Specifying theorem provers in a higher-order logic programming language, Ninth International Conference on Automated Deduction, number 310 in LNCS, pp.61-80, 1988.
DOI : 10.1007/BFb0012823

A. Felty and A. Momigliano, Hybrid, Journal of Automated Reasoning, vol.18, issue.1, pp.43-105, 2012.
DOI : 10.1017/S0956796807006557

A. P. Felty, A. Momigliano, and B. Pientka, The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations, Journal of Automated Reasoning, vol.10, issue.4, 2015.
DOI : 10.1145/2103656.2103709

J. Gabbay and A. M. Pitts, A new approach to abstract syntax involving binders, Proceedings. 14th Symposium on Logic in Computer Science (Cat. No. PR00158), pp.214-224, 1999.
DOI : 10.1109/LICS.1999.782617

A. Gacek, The Abella Interactive Theorem Prover (System Description), Fourth International Joint Conference on Automated Reasoning, pp.154-161, 2008.
DOI : 10.1007/978-3-540-71070-7_13

A. Gacek, D. Miller, and G. Nadathur, Reasoning in Abella about Structural Operational Semantics Specifications, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pp.85-100, 2008.
DOI : 10.1016/j.entcs.2008.12.118

A. Gacek, D. Miller, and G. Nadathur, Nominal abstraction. Information and Computation, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004
URL : https://doi.org/10.1016/j.ic.2010.09.004

A. Gacek, D. Miller, and G. Nadathur, A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012.
DOI : 10.1007/s10817-008-9097-2
URL : https://hal.archives-ouvertes.fr/hal-00776208

U. Gérard and D. Miller, Separating functional computation from relations, 26th EACSL Annual Conference on Computer Science Logic, 2017.

K. Gödel, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte der Mathematischen Physik, pp.173-198, 1931.

J. C. Gordon and T. F. Melham, Introduction to HOL ? A theorem proving environment for higher order logic, 1993.

M. J. Gordon, A. J. Milner, and C. P. Wadsworth, Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol.78, 1979.
DOI : 10.1007/3-540-09724-4

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

F. Honsell, M. Miculan, and I. Scagnetto, ??-calculus in (Co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2001.
DOI : 10.1016/S0304-3975(00)00095-5

G. Klein, K. Elphinstone, G. Heiser-andronick, D. Cock, P. Derrin et al., seL4, Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, SOSP '09, pp.207-220, 2009.
DOI : 10.1145/1629575.1629596

X. Leroy, Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, pp.107-115, 2009.
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861

G. Liang, X. Nadathur, and . Qi, Choices in Representation and Reduction Strategies for Lambda Terms in Intensional Contexts, Journal of Automated Reasoning, vol.198, issue.1?2, pp.89-132, 2005.
DOI : 10.1016/1385-7258(72)90034-0

D. Mackenzie, Mechanizing Proof, 2001.

. Martin-löf, Intuitionistic Type Theory. Studies in Proof Theory Lecture Notes, Bibliopolis, 1984.

R. Mcdowell and D. Miller, A logic for reasoning with higher-order abstract syntax, Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp.434-445, 1997.
DOI : 10.1109/LICS.1997.614968

R. Mcdowell and D. Miller, Cut-elimination for a logic with definitions and induction, Theoretical Computer Science, vol.232, issue.1-2, pp.91-119, 2000.
DOI : 10.1016/S0304-3975(99)00171-1

R. Mcdowell and D. Miller, Reasoning with higher-order abstract syntax in a logical framework, ACM Transactions on Computational Logic, vol.3, issue.1, pp.80-136, 2002.
DOI : 10.1145/504077.504080

. Miller, An extension to ML to handle bound variables in data structures: Preliminary report, Informal Proceedings of the Logical Frameworks BRA Workshop, 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

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

. Miller, Finding unity in computational logic, Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS '10, pp.1-3, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00772557

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

G. Miller, F. Nadathur, A. Pfenning, and . Scedrov, Uniform proofs as a foundation for logic programming, Annals of Pure and Applied Logic, vol.51, issue.1-2, pp.125-157, 1991.
DOI : 10.1016/0168-0072(91)90068-W

D. Miller and A. Tiu, A proof theory for generic judgments, 55 Robin Milner. Communication and Concurrency, pp.749-783, 1989.
DOI : 10.1145/1094622.1094628

R. Milner, Communicating and Mobile Systems: The ?-Calculus, 1999.

A. Momigliano and A. Tiu, Induction and Co-induction in Sequent Calculus, Post-proceedings of TYPES 2003, number 3085 in LNCS, pp.293-308, 2003.
DOI : 10.1007/978-3-540-24849-1_19

S. Moore, A mechanically verified language implementation, Journal of Automated Reasoning, vol.5, issue.4, pp.461-49215, 1989.
DOI : 10.1007/BF00243133

G. Nadathur and D. J. Mitchell, System Description: Teyjus???A Compiler and Abstract Machine Based Implementation of ??Prolog, 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pp.287-291, 1999.
DOI : 10.1007/3-540-48660-7_25

G. Nadathur and D. S. Wilson, A notation for lambda terms a generalization of environments, Theoretical Computer Science, vol.198, issue.1-2, pp.49-98, 1998.
DOI : 10.1016/S0304-3975(97)00184-9

C. Lawrence and . Paulson, A generic tableau prover and its integration with isabelle, J. UCS, vol.5, issue.3, pp.73-87, 1999.

A. J. Perlis, Epigrams on programming, ACM SIGPLAN Notices, pp.7-13, 1982.

F. Pfenning, Logic programming in the LF logical framework, Logical Frameworks, pp.149-181, 1991.
DOI : 10.1017/CBO9780511569807.008

F. Pfenning and C. Elliott, Higher-order abstract syntax 65 Frank Pfenning and Carsten Schürmann. System description: Twelf ? A meta-logical framework for deductive systems, Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation 16th Conf. on Automated Deduction (CADE), number 1632 in LNAI, pp.199-208, 1988.

B. Pientka and J. Dunfield, Beluga: A framework for programming and reasoning with deductive systems (system description) 67 The POPLmark Challenge webpage, Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pp.15-21, 2010.

F. Pottier, An Overview of C??ml, Electronic Notes in Theoretical Computer Science, vol.148, issue.2, pp.27-51, 2005.
DOI : 10.1016/j.entcs.2005.11.039

D. Pous, Weak bisimulation upto elaboration, LNCS, vol.4137, pp.390-405, 2006.

D. Pous, Complete lattices and upto techniques, LNCS, vol.4807, pp.351-366, 2007.
DOI : 10.1007/978-3-540-76637-7_24
URL : https://hal.archives-ouvertes.fr/ensl-00155308

D. Pous and D. Sangiorgi, Enhancements of the bisimulation proof method, Advanced Topics in Bisimulation and Coinduction, pp.233-289, 2011.
DOI : 10.1017/CBO9780511792588.007
URL : https://hal.archives-ouvertes.fr/hal-00909391

A. Qi, S. Gacek, G. Holte, Z. Nadathur, and . Snow, The Teyjus system ? version 2, 2015.

D. Sangiorgi, ??-Calculus, internal mobility, and agent-passing calculi, Theoretical Computer Science, vol.167, issue.1-2, pp.235-274, 1996.
DOI : 10.1016/0304-3975(96)00075-8

H. Schwichtenberg and . Minlog, The Seventeen Provers of the World, LNCS, vol.3600, pp.151-157, 2006.

P. Sewell, F. Z. Nardelli, S. Owens, G. Peskine, T. Ridge et al., Ott: Effective tool support for the working semanticist, Journal of Functional Programming, vol.8, issue.01, pp.71-122, 2010.
DOI : 10.1007/BFb0035382

Z. Snow, D. Baelde, and G. Nadathur, A meta-programming approach to realizing dependently typed logic programming, Proceedings of the 12th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '10, pp.187-198, 2010.
DOI : 10.1145/1836089.1836113

M. Southern and K. Chaudhuri, A two-level logic approach to reasoning about typed specification languages, 34th International Conference on Foundations of Software Technology and Theoretical Computer XX:16 Mechanized Metatheory Revisited: An Extended Abstract Science (FSTTCS), volume 29 of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.557-569, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01091544

A. Tiu, Model Checking for ??-Calculus Using Proof Search, Proceedings of CONCUR'05, pp.36-50, 2005.
DOI : 10.1007/11539452_7

A. Tiu and D. Miller, A Proof Search Specification of the ??-Calculus, 3rd Workshop on the Foundations of Global Ubiquitous Computing, pp.79-101, 2005.
DOI : 10.1016/j.entcs.2005.05.006

A. Tiu and D. Miller, Proof search specifications of bisimulation and modal logics for the ??-calculus, ACM Transactions on Computational Logic, vol.11, issue.2, p.2010
DOI : 10.1145/1656242.1656248

A. Tiu and A. Momigliano, Cut elimination for a logic with induction and co-induction, Journal of Applied Logic, vol.10, issue.4, pp.330-367, 2012.
DOI : 10.1016/j.jal.2012.07.007

C. Urban, Nominal Techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.323, issue.1???2, pp.327-356, 2008.
DOI : 10.1145/1183278.1183280

J. Van and H. , From Frege to Gödel: A Source Book in Mathematics, 1879-1931. Source books in the history of the sciences series, 1967.

M. Vaninwegen, The Machine-Assisted Proof of Programming Language Properties, 1996.