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
Encoding Modal Logics in Logical Frameworks, Studia Logica, vol.60, issue.1, pp.161-208, 1998. ,
DOI : 10.1023/A:1005060022386
Lambda Calculus: its Syntax and Semantics, 1984. ,
Lambda Calculi with Types, Handbook of Logic in Computer Science, volume II, pp.118-310, 1992. ,
DOI : 10.1017/cbo9781139032636
Autarkic computations in formal proofs, Journal of Automated Reasoning, vol.28, issue.3, pp.321-336, 2002. ,
DOI : 10.1023/A:1015761529444
Pure Pattern Type Systems, POPL'03, pp.250-261, 2003. ,
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
What the Tortoise Said to Achilles. Mind, pp.278-280 ,
Library reflection ,
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
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
Higher-order representation of substructural logics, ICFP '10, pp.131-142, 2010. ,
AUTOMATH, a Language for Mathematics, Automation and Reasoning, pp.159-200, 1967. ,
DOI : 10.1007/978-3-642-81955-1_11
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
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
A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
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
Maksimovic, and I. Scagnetto. LFP ? a logical framework with external predicates ,
Maksimovic, and I. Scagnetto. LFP ? a logical framework with external predicates, Proceedings of LFMTP 2012. ACM Digital Library ,
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
??-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
A universe of binding and computation, ICFP '09, pp.123-134, 2009. ,
Design by contract, Advances in Object-Oriented Software Engineering, pp.1-50, 1991. ,
Contextual Model Type Theory, ACM Transactions on Computational Logic, vol.9, issue.3, 2008. ,
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
Twelf user's guide, chapter 6: Constraint domains, 2013. ,
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
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
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
La Science et l'Hypothèse. Flammarion, 1902. ,
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
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
Il mondo come volontà e rappresentazione ,
Proof checking technology for satisfiability modulo theories In International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, pp.121-133, 2008. ,
Higher-Order Rewriting with Dependent Types, 1999. ,
A Concurrent Logical Framework I: Judgments and Properties, 2002. ,