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. ,
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
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
Higher-order representation of substructural logics, ICFP '10, pp.131-142, 2010. ,
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, Preliminary version in Proc. of LICS'87, pp.143-184, 1993. ,
DOI : 10.1145/138027.138060
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
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
Maksimovic, and I. Scagnetto. LF P ? a logical framework with external predicates ,
A universe of binding and computation, ICFP '09, pp.123-134, 2009. ,
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
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
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
Natural deduction for intuitionistic noncommutative linear logic, TLCA'99, pp.644-644, 1999. ,
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
Proof checking technology for satisfiability modulo theories In International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, pp.121-133, 2008. ,
A Concurrent Logical Framework I: Judgments and Properties, 2002. ,