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

A. Avron, F. Honsell, M. Miculan, and C. Paravano, Encoding Modal Logics in Logical Frameworks, Studia Logica, vol.60, issue.1, pp.161-208, 1998.
DOI : 10.1023/A:1005060022386

H. Barendregt, Lambda Calculus: its Syntax and Semantics, 1984.

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

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

F. Blanqui, J. Jouannaud, and P. Strub, From Formal Proofs to Mathematical Proofs: A Safe, Incremental Way for Building in First-order Decision Procedures, IFIP TCS, pp.349-365, 2008.
DOI : 10.1007/978-0-387-09680-3_24
URL : https://hal.archives-ouvertes.fr/inria-00275382

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

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

G. Dowek, T. Hardin, and C. Kirchner, Theorem proving modulo, Journal of Automated Reasoning, vol.31, issue.1, pp.33-72, 2003.
DOI : 10.1023/A:1027357912519
URL : https://hal.archives-ouvertes.fr/hal-01199506

J. Filliâtre and C. Marché, The Why/Krakatoa/Caduceus Platform for Deductive Program Verification, CAV'07, 2007.
DOI : 10.1007/978-3-540-73368-3_21

R. Harper, F. Honsell, and G. Plotkin, A framework for defining logics, Preliminary version in Proc. of LICS'87, 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 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

D. Licata and R. Harper, A universe of binding and computation, ICFP '09, pp.123-134, 2009.

A. Nanevski, F. Pfenning, and B. Pientka, Contextual Model Type Theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008.

F. Pfenning, Intensionality, extensionality, and proof irrelevance in modal type theory, Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, pp.221-230, 1993.
DOI : 10.1109/LICS.2001.932499

B. Pientka and J. Dunfield, Programming with proofs and explicit contexts, Proceedings of the 10th international ACM SIGPLAN symposium on Principles and practice of declarative programming, PPDP '08, pp.163-173, 2008.
DOI : 10.1145/1389449.1389469
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.158.8383

J. Polakow and F. Pfenning, Natural Deduction for Intuitionistic Non-commutative Linear Logic, TLCA'99, pp.644-644, 1999.
DOI : 10.1007/3-540-48959-2_21
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.36.5390

K. Watkins, I. Cervesato, F. Pfenning, and D. Walker, A Concurrent Logical Framework I: Judgments and Properties, 2002.
DOI : 10.1007/978-3-540-24849-1_23
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7276