A. Avron, F. Honsell, I. A. Mason, and R. Pollack, Using typed lambda calculus to implement formal systems on a machine, Journal of Automated Reasoning, vol.49, issue.3, pp.309-354, 1992.
DOI : 10.1007/BF00245294

H. Barendregt, Lambda Calculi with Types, Handbook of Logic in Computer Science, pp.118-310, 1992.

H. P. Barendregt and E. Barendsen, Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002.
DOI : 10.1023/A:1015761529444

H. Barendregt, W. Dekkers, and R. Statman, Perspectives in Logic: Lambda Calculus with Types, Cambridge UP, 2013.

B. Barras, Coq en Coq, Projet COQ, 1996.
URL : https://hal.archives-ouvertes.fr/inria-00073667

G. Barthe, H. Cirstea, C. Kirchner, and L. Liquori, Pure Pattern Type Systems, POPL'03, pp.250-261, 2003.

R. Boulton, A. Gordon, M. Gordon, J. Harrison, J. Herbert et al., Experience with embedding hardware description languages in HOL, See Stavridou, Melham, and Boute, pp.129-156, 1992.

L. Carroll, What the Tortoise Said to Achilles. Mind, pp.278-280

I. Cervesato and F. Pfenning, A linear logical framework, Logic in Computer Science Proc. of LICS'96, 1996.
DOI : 10.1006/inco.2001.2951
URL : http://doi.org/10.1006/inco.2001.2951

H. Cirstea, C. Kirchner, and L. Liquori, The Rho Cube, FOSSACS'01, pp.166-180, 2001.
DOI : 10.1007/3-540-45315-6_11
URL : https://hal.archives-ouvertes.fr/inria-00107877

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

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Proc. of TLCA, pp.102-117, 2007.
DOI : 10.1007/978-3-540-73228-0_9

K. Crary, Higher-order representation of substructural logics, ICFP '10, pp.131-142, 2010.

N. De-bruijn, AUTOMATH, a Language for Mathematics, Automation and Reasoning, pp.159-200, 1967.
DOI : 10.1007/978-3-642-81955-1_11

J. Despeyroux, A. Felty, and A. , Hirschowitz Higher-order abstract syntax in Coq, TLCA'95, 1995.

A. D. Gordon and T. Melham, Five Axioms of Alpha-Conversion. Theorem proving in higher order logics, pp.173-190, 1996.

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

R. Harper and D. Licata, Mechanizing metatheory in a logical framework, Journal of Functional Programming, vol.40, issue.4-5, pp.613-673, 2007.
DOI : 10.1006/inco.2001.2951

F. Honsell, M. Lenisa, and L. Liquori, A Framework for Defining Logical Frameworks, Electronic Notes in Theoretical Computer Science, vol.172, pp.399-436, 2007.
DOI : 10.1016/j.entcs.2007.02.014
URL : https://hal.archives-ouvertes.fr/hal-01148312

F. Honsell, M. Lenisa, L. Liquori, and P. , Maksimovic, and I. Scagnetto. LF P ? a logical framework with external predicates, Proc. of LFMTP 2012

F. Honsell, M. Lenisa, L. Liquori, and I. Scagnetto, A Conditional Logical Framework, LPAR'08, pp.143-157, 2008.
DOI : 10.1007/978-3-540-89439-1_10
URL : https://hal.archives-ouvertes.fr/hal-00909574

A. Bucalo, M. Hofmann, F. Honsell, M. Miculan, and I. Scagnetto, Consistency of the theory of contexts, Journal of Functional Programming, vol.16, issue.03, pp.327-395, 2006.
DOI : 10.1017/S0956796806005892

F. Pfenning and C. Schuermann, Twelf user's guide, version 1.2, 1998.

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

H. Poincaré, La Science et l'Hypothèse. Flammarion, 1902.

J. Polakow and F. Pfenning, Natural deduction for intuitionistic noncommutative linear logic, TLCA'99, 1581, pp.644-644, 1999.

C. Röckl, D. Hirschkoff, and S. Berghofer, HOAS with induction in Isabelle/HOL: Formalizing the ?-calculus and mechanizing the theory of contexts, FoSSaCS, pp.364-378, 2001.

K. Watkins, I. Cervesato, F. Pfenning, and D. Walker, A Concurrent Logical Framework I: Judgments and Properties, 2002.