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. 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, FOS- SACS'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

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

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, 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. 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

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

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

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

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

A. Poswolsky and C. Schürmann, System Description: Delphin ??? A Functional Programming Language for Deductive Systems, Electronic Notes in Theoretical Computer Science, vol.228, pp.113-120, 2009.
DOI : 10.1016/j.entcs.2008.12.120

A. Stump, Proof checking technology for satisfiability modulo theories In International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, pp.121-133, 2008.

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