Journal Article Stateful authorization logic - Proof theory and a case study 2012 • Journal of Computer Security • 20(4):353-391 Garg D, Pfenning F
Conference Towards concurrent type theory 2012 • Conference Record of the Annual ACM Symposium on Principles of Programming Languages • 1-12 Caires L, Pfenning F, Toninho B
Conference Trace matching in a concurrent logical framework 2012 1-12 Cervesato I, Pfenning F, Sacchini JL, Schürmann C, Simmons RJ
Conference Dependent Session Types via Intuitionistic Linear Type Theory 2011 • PPDP 11 - PROCEEDINGS OF THE 2011 SYMPOSIUM ON PRINCIPLES AND PRACTICES OF DECLARATIVE PROGRAMMING • 161-171 Toninho B, Caires L, Pfenning F
Conference Logical approximation for program analysis 2011 • Higher-Order and Symbolic Computation • 24(1-2):41-80 Simmons RJ, Pfenning F
Conference Proof-Carrying Code in a Session-Typed Process Calculus 2011 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 7086:21-36 Pfenning F, Caires L, Toninho B
Conference Stateful Authorization Logic: Proof Theory and a Case Study 2011 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 6710:210-225 Garg D, Pfenning F
Conference A Proof-Carrying File System 2010 • IEEE Symposium on Security and Privacy: Proceedings • 349-364 Garg D, Pfenning F
Journal Article Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance 2010 • Logical Methods in Computer Science • 5:2010 Lovas W, Pfenning F
Journal Article REFINEMENT TYPES FOR LOGICAL FRAMEWORKS AND THEIR INTERPRETATION AS PROOF IRRELEVANCE 2010 • Logical Methods in Computer Science • 6(4): Lovas W, Pfenning F
Preprint Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance 2010 Lovas W, Pfenning F
Conference Session Types as Intuitionistic Linear Propositions 2010 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 6269:222-+ Caires L, Pfenning F
Journal Article The Practice and Promise of Substructural Frameworks 2010 • Electronic Proceedings in Theoretical Computer Science • Pfenning F
Journal Article A Logical Representation of Common Rules for Controlling Access to Classified Information 2009 Garg D, Serenyi D, Pfenning F, Witten B
Conference Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method 2009 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 5663:230-244 McLaughlin S, Pfenning F
Journal Article Intuitionistic Letcc via Labelled Deduction 2009 • Electronic Notes in Theoretical Computer Science • 231:91-111 Reed J, Pfenning F
Conference Refinement Types as Proof Irrelevance 2009 • Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) • 5608:157-171 Lovas W, Pfenning F
Conference Substructural Operational Semantics as Ordered Logic Programming 2009 • Proceedings - Symposium on Logic in Computer Science • 101-110 Pfenning F, Simmons RJ
Journal Article A Bidirectional Refinement Type System for LF 2008 • Electronic Notes in Theoretical Computer Science • 196:113-128 Lovas W, Pfenning F
Conference A logical characterization of forward and backward chaining in the inverse method 2008 • Journal of Automated Reasoning • 40(2-3):133-177 Chaudhuri K, Pfenning F, Price G
