Journal Article A linear logical framework 2002 • Information and Computation • 179(1):19-75 Cervesato I, Pfenning F
Journal Article Editorial 2002 • ACM Transactions on Computational Logic • 3(3):335 Abadi M, Libkin L, Pfenning F
Conference Electronic Notes in Theoretical Computer Science: Preface 2002 • Electronic Notes in Theoretical Computer Science • 70(2):1 Pfenning F
Conference Logical frameworks - A brief introduction 2002 • PROOF AND SYSTEM-RELIABILITY • 62:137-166 Pfenning F
Conference Trustless Grid computing in ConCert 2002 • Lecture Notes in Computer Science • 2536:112-125 Chang BYE, Crary K, DeLap M, Harper R, Liszka J, Murphy T, Pfenning F
Journal Article A judgmental reconstruction of modal logic 2001 • Mathematical Structures in Computer Science • 11(4):511-540 Pfenning F, Davies R
Journal Article A modal analysis of staged computation 2001 • Journal of the ACM • 48(3):555-604 Davies R, Pfenning F
Preprint Higher-Order Pattern Complement and the Strict Lambda-Calculus 2001 Momigliano A, Pfenning F
Conference Intensionality, extensionality, and proof irrelevance in modal type theory 2001 • Proceedings - Symposium on Logic in Computer Science • 221-230 Pfenning F
Journal Article Primitive recursion for higher-order abstract syntax 2001 • Theoretical Computer Science • 266(1-2):1-57 Schürmann C, Despeyroux J, Pfenning F
Conference Automated techniques for provably safe mobile code 2000 • Proceedings - DARPA Information Survivability Conference and Exposition, DISCEX 2000 • 1:406-419 Crary K, Harper R, Lee P, Pfenning F
Journal Article Editorial: Strategies in Automated Deduction 2000 • Annals of Mathematics and Artificial Intelligence • 29(1-4): Gramlich B, Kirchner H, Pfenning F
Journal Article Efficient resource management for linear logic proof search 2000 • Theoretical Computer Science • 232(1-2):133-163 Cervesato I, Hodas JS, Pfenning F
Journal Article Intersection types and computational effects 2000 • ACM Sigplan Notices • 35(9):198-208 Davies R, Pfenning F
Conference Intersection types and computational effects 2000 • ACM Sigplan Notices • 35(9):198-208 Davies R, Pfenning F
Conference On the logical foundations of staged computation 2000 • Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation • 33 Pfenning F
Conference Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Pratice of Declarative Programming: Preface 2000 • Proceedings of the 2nd International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming Gabbrielli M, Pfenning F
Conference Reasoning about staged computation - Abstract of invited talk 2000 • Lecture Notes in Computer Science • 1924:5-6 Pfenning F
Journal Article Structural cut elimination I. Intuitionistic and classical logic 2000 • Information and Computation • 157(1-2):84-141 Pfenning F
Chapter Algorithms for Equality and Unification in the Presence of Notational Definitions 1999 • Lecture Notes in Computer Science • 1657:179-193 Pfenning F, Schürmann C
Journal Article Dependent types in practical programming 1999 • Conference Record of the Annual ACM Symposium on Principles of Programming Languages • 214-227 Xi H, Pfenning F
Conference Logical and meta-logical frameworks 1999 • Lecture Notes in Computer Science • 1702:206 Pfenning F