Frank Pfenning

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho: Behavioral Polymorphism and Parametricity in Session-Based Communication. ESOP 2013: 330-349

Bernardo Toninho, Luís Caires, Frank Pfenning: Higher-Order Processes, Functions, and Sessions: A Monadic Integration. ESOP 2013: 350-369

Frank Pfenning (Ed.): Foundations of Software Science and Computation Structures - 16th International Conference, FOSSACS 2013, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2013, Rome, Italy, March 16-24, 2013. Proceedings. Lecture Notes in Computer Science 7794, Springer 2013, isbn 978-3-642-37074-8

Deepak Garg, Frank Pfenning: Stateful authorization logic - Proof theory and a case study. Journal of Computer Security 20(4): 353-391 (2012)

Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho: Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. CSL 2012: 228-242

Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho: Linear Logical Relations for Session-Based Concurrency. ESOP 2012: 539-558

Bernardo Toninho, Luís Caires, Frank Pfenning: Functions as Session-Typed Processes. FoSSaCS 2012: 346-360

Luís Caires, Frank Pfenning, Bernardo Toninho: Towards concurrent type theory. TLDI 2012: 1-12

Robert J. Simmons, Frank Pfenning: Logical approximation for program analysis. Higher-Order and Symbolic Computation 24(1-2): 41-80 (2011)

Frank Pfenning, Luís Caires, Bernardo Toninho: Proof-Carrying Code in a Session-Typed Process Calculus. CPP 2011: 21-36

Bernardo Toninho, Luís Caires, Frank Pfenning: Dependent session types via intuitionistic linear type theory. PPDP 2011: 161-172

Jamie Morgenstern, Deepak Garg, Frank Pfenning: A Proof-Carrying File System with Revocable and Use-Once Certificates. STM 2011: 40-55

William Lovas, Frank Pfenning: Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance. Logical Methods in Computer Science 6(4) (2010)

Luís Caires, Frank Pfenning: Session Types as Intuitionistic Linear Propositions. CONCUR 2010: 222-236

Deepak Garg, Frank Pfenning: A Proof-Carrying File System. IEEE Symposium on Security and Privacy 2010: 349-364

Deepak Garg, Frank Pfenning: Stateful Authorization Logic: - Proof Theory and a Case Study. STM 2010: 210-225

Jason Reed, Frank Pfenning: Intuitionistic Letcc via Labelled Deduction. Electr. Notes Theor. Comput. Sci. 231: 91-111 (2009)

Sean McLaughlin, Frank Pfenning: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. CADE 2009: 230-244

Frank Pfenning, Robert J. Simmons: Substructural Operational Semantics as Ordered Logic Programming. LICS 2009: 101-110

Robert J. Simmons, Frank Pfenning: Linear logical approximations. PEPM 2009: 9-20

William Lovas, Frank Pfenning: Refinement Types as Proof Irrelevance. TLCA 2009: 157-171

William Lovas, Frank Pfenning: A Bidirectional Refinement Type System for LF. Electr. Notes Theor. Comput. Sci. 196: 113-128 (2008)

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker: Specifying Properties of Concurrent Computations in CLF. Electr. Notes Theor. Comput. Sci. 199: 67-87 (2008)

Kaustuv Chaudhuri, Frank Pfenning, Greg Price: A Logical Characterization of Forward and Backward Chaining in the Inverse Method. J. Autom. Reasoning 40(2-3): 133-177 (2008)

Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka: Contextual modal type theory. ACM Trans. Comput. Log. 9(3) (2008)

Sungwoo Park, Frank Pfenning, Sebastian Thrun: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1) (2008)

Henry DeYoung, Deepak Garg, Frank Pfenning: An Authorization Logic With Explicit Time. CSF 2008: 133-145

Robert J. Simmons, Frank Pfenning: Linear Logical Algorithms. ICALP (2) 2008: 336-347

Sean McLaughlin, Frank Pfenning: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. LPAR 2008: 174-181

Frank Pfenning: Subtyping and intersection types revisited. ICFP 2007: 219

Uluc Saranli, Frank Pfenning: Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. ICRA 2007: 3705-3710

Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter: Consumable Credentials in Linear-Logic-Based Access-Control Systems. NDSS 2007

Frank Pfenning: On a Logical Foundation for Explicit Substitutions. RTA 2007: 19

Frank Pfenning: On a Logical Foundation for Explicit Substitutions. TLCA 2007: 1

Frank Pfenning (Ed.): Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings. Lecture Notes in Computer Science 4603, Springer 2007, isbn 978-3-540-73594-6

Kaustuv Chaudhuri, Frank Pfenning, Greg Price: A Logical Characterization of Forward and Backward Chaining in the Inverse Method. IJCAR 2006: 97-111

Deepak Garg, Frank Pfenning: Non-Interference in Constructive Authorization Logic. CSFW 2006: 283-296

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter: A Linear Logic of Authorization and Knowledge. ESORICS 2006: 297-312

Frank Pfenning (Ed.): Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings. Lecture Notes in Computer Science 4098, Springer 2006, isbn 3-540-36834-5

Karl Crary, Aleksey Kliger, Frank Pfenning: A monadic analysis of information flow security with mutable state. J. Funct. Program. 15(2): 249-291 (2005)

Aleksandar Nanevski, Frank Pfenning: Staged computation with names and necessity. J. Funct. Program. 15(5): 893-939 (2005)

Robert Harper, Frank Pfenning: On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1): 61-101 (2005)

Kaustuv Chaudhuri, Frank Pfenning: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. CADE 2005: 69-83

Deepak Garg, Frank Pfenning: Type-Directed Concurrency. CONCUR 2005: 6-20

Kaustuv Chaudhuri, Frank Pfenning: Focusing the Inverse Method for Linear Logic. CSL 2005: 200-215

Frank Pfenning: Towards a type theory of contexts. MERLIN 2005: 1

Sungwoo Park, Frank Pfenning, Sebastian Thrun: A probabilistic language based upon sampling functions. POPL 2005: 171-182

Pablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins: Monadic concurrent linear logic programming. PPDP 2005: 35-46

Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi: ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reasoning 32(1): 75-92 (2004)

Frank Pfenning: Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). APLAS 2004: 196

Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning: A Symmetric Modal Lambda Calculus for Distributed Computing. LICS 2004: 286-295

Joshua Dunfield, Frank Pfenning: Tridirectional typechecking. POPL 2004: 281-292

Penny Anderson, Frank Pfenning: Verifying Uniqueness in a Logical Framework. TPHOLs 2004: 18-33

Iliano Cervesato, Frank Pfenning: A Linear Spine Calculus. J. Log. Comput. 13(5): 639-688 (2003)

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning: Automated techniques for provably safe mobile code. Theor. Comput. Sci. 290(2): 1175-1199 (2003)

Alberto Momigliano, Frank Pfenning: Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. 4(4): 493-529 (2003)

Brigitte Pientka, Frank Pfenning: Optimizing Higher-Order Pattern Unification. CADE 2003: 473-487

Joshua Dunfield, Frank Pfenning: Type Assignment for Intersections and Unions in Call-by-Value Languages. FoSSaCS 2003: 250-266

Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning: A modal foundation for meta-variables. MERLIN 2003

Sebastian Thrun, Geoffrey J. Gordon, Frank Pfenning, Mary Berna, Brennan Sellner, Brad Lisien: A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data. IJCAI 2003: 1427-1428

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning: A type theory for memory allocation and data layout. POPL 2003: 172-184

Carsten Schürmann, Frank Pfenning: A Coverage Checking Algorithm for LF. TPHOLs 2003: 120-135

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker: A Concurrent Logical Framework: The Propositional Fragment. TYPES 2003: 355-377

Frank Pfenning, Yannis Smaragdakis (Eds.): Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings. Lecture Notes in Computer Science 2830, Springer 2003, isbn 3-540-20102-5

Frank Pfenning: Invited talk: Tri-Directional Type Checking. Electr. Notes Theor. Comput. Sci. 70(1) (2002)

Frank Pfenning: Preface. Electr. Notes Theor. Comput. Sci. 70(2): 146 (2002)

Iliano Cervesato, Frank Pfenning: A Linear Logical Framework. Inf. Comput. 179(1): 19-75 (2002)

Martín Abadi, Leonid Libkin, Frank Pfenning: Editorial. ACM Trans. Comput. Log. 3(3): 335-335 (2002)

Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning: Trustless Grid Computing in ConCert. GRID 2002: 112-125

Rowan Davies, Frank Pfenning: A modal analysis of staged computation. J. ACM 48(3): 555-604 (2001)

Frank Pfenning, Rowan Davies: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4): 511-540 (2001)

Carsten Schürmann, Joëlle Despeyroux, Frank Pfenning: Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1-2): 1-57 (2001)

Frank Pfenning: Logical Frameworks. Handbook of Automated Reasoning 2001: 1063-1147

Frank Pfenning: Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. LICS 2001: 221-230

Alberto Momigliano, Frank Pfenning: Higher-Order Pattern Complement and the Strict Lambda-Calculus. CoRR cs.LO/0109072 (2001)

Robert Harper, Frank Pfenning: On Equivalence and Canonical Forms in the LF Type Theory. CoRR cs.LO/0110028 (2001)

Bernhard Gramlich, Hélène Kirchner, Frank Pfenning: Editorial: Strategies in Automated Deduction. Ann. Math. Artif. Intell. 29(1-4): 0- (2000)

Frank Pfenning: Structural Cut Elimination: I. Intuitionistic and Classical Logic. Inf. Comput. 157(1-2): 84-141 (2000)

Iliano Cervesato, Joshua S. Hodas, Frank Pfenning: Efficient resource management for linear logic proof search. Theor. Comput. Sci. 232(1-2): 133-163 (2000)

Rowan Davies, Frank Pfenning: Intersection types and computational effects. ICFP 2000: 198-208

Frank Pfenning: On the Logical Foundations of Staged Computation (Abstract of Invited Talk). PEPM 2000: 33

Frank Pfenning: Reasoning about Staged Computation. SAIG 2000: 5-6

J. Polokow, Frank Pfenning: Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. Electr. Notes Theor. Comput. Sci. 20: 449-466 (1999)

Olivier Danvy, Belmina Dzafic, Frank Pfenning: On proving syntactic properties of CPS programs. Electr. Notes Theor. Comput. Sci. 26: 21-33 (1999)

Alberto Momigliano, Frank Pfenning: The Relative Complement Problem for Higher-Order Patterns. APPIA-GULP-PRODE 1999: 497-512

Frank Pfenning, Carsten Schürmann: System Description: Twelf - A Meta-Logical Framework for Deductive Systems. CADE 1999: 202-206

Alberto Momigliano, Frank Pfenning: The Relative Complement Problem for Higher-Order Patterns. ICLP 1999: 380-394

Hongwei Xi, Frank Pfenning: Dependent Types in Practical Programming. POPL 1999: 214-227

Frank Pfenning: Logical and Meta-Logical Frameworks (Abstract). PPDP 1999: 206

Jeff Polakow, Frank Pfenning: Natural Deduction for Intuitionistic Non-communicative Linear Logic. TLCA 1999: 295-309

Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies: Modal Types as Staging Specifications for Run-Time Code Generation. ACM Comput. Surv. 30(3es): 8 (1998)

Frank Pfenning, Carsten Schürmann: Algorithms for Equality and Unification in the Presence of Notational Definitions. Electr. Notes Theor. Comput. Sci. 17: 1-13 (1998)

Robert Harper, Frank Pfenning: A Module System for a Programming Language Based on the LF Logical Framework. J. Log. Comput. 8(1): 5-31 (1998)

Wilfried Sieg, Frank Pfenning: Note by the Guest Editors. Studia Logica 60(1): 1 (1998)

Frank Pfenning: Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). CADE 1998: 1-2

Carsten Schürmann, Frank Pfenning: Automated Theorem Proving in a Simple Meta-Logic for LF. CADE 1998: 286-300

Philip Wickline, Peter Lee, Frank Pfenning: Run-time Code Generation and Modal-ML. PLDI 1998: 224-235

Hongwei Xi, Frank Pfenning: Eliminating Array Bound Checking Through Dependent Types. PLDI 1998: 249-257

Frank Pfenning, Carsten Schürmann: Algorithms for Equality and Unification in the Presence of Notational Definitions. TYPES 1998: 179-193

Paliath Narendran, Frank Pfenning, Richard Statman: On the Unification Problem for Cartesian Closed Categories. J. Symb. Log. 62(2): 636-647 (1997)

Iliano Cervesato, Frank Pfenning: Linear Higher-Order Pre-Unification. LICS 1997: 422-433

Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann: Primitive Recursion for Higher-Order Abstract Syntax. TLCA 1997: 147-163

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi: TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reasoning 16(3): 321-353 (1996)

Frank Pfenning: The Practice of Logical Frameworks. CAAP 1996: 119-134

Iliano Cervesato, Joshua S. Hodas, Frank Pfenning: Efficient Resource Management for Linear Logic Proof Search. ELP 1996: 67-81

Ekkehard Rohwedder, Frank Pfenning: Mode and Termination Checking for Higher-Order Logic Programs. ESOP 1996: 296-310

Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning: Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP 1996: 259-273

Iliano Cervesato, Frank Pfenning: A Linear Logical Framework. LICS 1996: 264-275

Rowan Davies, Frank Pfenning: A Modal Analysis of Staged Computation. POPL 1996: 258-270

Frank Pfenning, Hao-Chi Wong: On a modal lambda calculus for S4. Electr. Notes Theor. Comput. Sci. 1: 515-534 (1995)

Frank Pfenning: Structural Cut Elimination. LICS 1995: 156-166

Frank Pfenning: Elf: A Meta-Language for Deductive Systems (System Descrition). CADE 1994: 811-815

Frank Pfenning (Ed.): Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings. Lecture Notes in Computer Science 822, Springer 1994, isbn 3-540-58216-9

Frank Pfenning: On the Undecidability of Partial Polymorphic Type Reconstruction. Fundam. Inform. 19(1/2): 185-199 (1993)

Paliath Narendran, Frank Pfenning, Richard Statman: On the Unification Problem for Cartesian Closed Categories. LICS 1993: 57-63

Spiro Michaylov, Frank Pfenning: Higher-Order Logic Programming as Constraint Logic Programming. PPCP 1993: 210-218

Michael Kohlhase, Frank Pfenning: Unification in a Lambda-Calculus with Intersection Types. ILPS 1993: 488-505

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi: TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. HUG 1993: 366-370

Scott Dietzen, Frank Pfenning: Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. Machine Learning 9: 23-55 (1992)

Gopalan Nadathur, Frank Pfenning: The Type System of a Higher-Order Logic Programming Language. Types in Logic Programming 1992: 245-283

Frank Pfenning: Dependent Types in Logic Programming. Types in Logic Programming 1992: 285-311

Frank Pfenning, Ekkehard Rohwedder: Implementing the Meta-Theory of Deductive Systems. CADE 1992: 537-551

John Hannan, Frank Pfenning: Compiler Verification in LF. LICS 1992: 407-418

Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov: Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Logic 51(1-2): 125-157 (1991)

Frank Pfenning, Peter Lee: Metacircularity in the Polymorphic lambda-Calculus. Theor. Comput. Sci. 89(1): 137-159 (1991)

Spiro Michaylov, Frank Pfenning: Natural Semantics and Some of Its Meta-Theory in Elf. ELP 1991: 299-344

Frank Pfenning: Unification and Anti-Unification in the Calculus of Constructions. LICS 1991: 74-85

Spiro Michaylov, Frank Pfenning: Compiling the Polymorphic Lambda-Calculus. PEPM 1991: 285-296

Tim Freeman, Frank Pfenning: Refinement Types for ML. PLDI 1991: 268-277

Scott Dietzen, Frank Pfenning: A Declarative Alternative to "Assert" in Logic Programming. ISLP 1991: 372-386

Frank Pfenning, Dan Nesmith: Presenting Intuitive Deductions via Symmetric Simplification. CADE 1990: 336-350

Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1990: 641-642

Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning: Tutorial on Lambda-Prolog. CADE 1990: 682

Frank Pfenning: Types in Logic Programming. ICLP 1990: 786

Scott Dietzen, Frank Pfenning: Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. ML 1989: 447-449

Frank Pfenning: Elf: A Language for Logic Definition and Verified Metaprogramming. LICS 1989: 313-322

Frank Pfenning, Christine Paulin-Mohring: Inductively Defined Types in the Calculus of Constructions. Mathematical Foundations of Programming Semantics 1989: 209-228

Frank Pfenning, Peter Lee: LEAP: A Language with Eval And Polymorphism. TAPSOFT, Vol.2 1989: 345-359

Frank Pfenning: Single Axioms in the Implicational Propositional Calculus. CADE 1988: 710-713

Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1988: 760-761

Frank Pfenning: Partial Polymorphic Type Inference and Higher-Order Unification. LISP and Functional Programming 1988: 153-163

Frank Pfenning, Conal Elliott: Higher-Order Abstract Syntax. PLDI 1988: 199-208

Peter Lee, Frank Pfenning, Gene Rollins, William L. Scherlis: The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments. Software Development Environments (SDE) 1988: 25-34

Robert L. Nord, Frank Pfenning: The Ergo Attribute System. Software Development Environments (SDE) 1988: 110-120

Peter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper: The TPS Theorem Proving System. CADE 1986: 663-664

Frank Pfenning: Analytic and Non-analytic Proofs. CADE 1984: 394-413