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, Lambda Calculi with Types, Handbook of Logic in Computer Science, volume II, pp.118-310, 1992.
DOI : 10.1017/cbo9781139032636

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

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

A. Chlipala, Library reflection

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

D. Cousineau and G. Dowek, Embedding Pure Type Systems in the Lambda-Pi-Calculus Modulo, Typed Lambda Calculi and Applications, 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

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, 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 P. , Maksimovic, and I. Scagnetto. LFP ? a logical framework with external predicates

F. Honsell, M. Lenisa, L. Liquori, and P. , Maksimovic, and I. Scagnetto. LFP ? a logical framework with external predicates, Proceedings of LFMTP 2012. ACM Digital Library

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 and M. , ??-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

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

B. Meyer, Design by contract, Advances in Object-Oriented Software Engineering, pp.1-50, 1991.

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

F. Pfenning and C. Schuermann, Twelf user's guide, chapter 6: Constraint domains, 2013.

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

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

G. D. Plotkin, Call-by-name, call-by-value and the ??-calculus, Theoretical Computer Science, vol.1, issue.2, pp.125-159, 1975.
DOI : 10.1016/0304-3975(75)90017-1

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

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

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. Shopenhauer, Il mondo come volontà e rappresentazione

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

R. Virga, Higher-Order Rewriting with Dependent Types, 1999.

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