| 2026 | IJCAR | Ordered Adjoint Logic. | Sophia Roshal, Frank Pfenning |
| 2025 | FSCD | Substructural Parametricity. | C. B. Aberl, Karl Crary, Chris Martens, Frank Pfenning |
| 2024 | Coordination | Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax). | Adrian Francalanza, Gerard Tabone, Frank Pfenning |
| 2024 | FSCD | Adjoint Natural Deduction. | Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka |
| 2023 | Coordination | Relating Message Passing and Shared Memory, Proof-Theoretically. | Frank Pfenning, Klaas Pruiksma |
| 2023 | FOSSACS | A Logical Framework with Higher-Order Rational (Circular) Terms. | Zhibo Chen, Frank Pfenning |
| 2023 | PPDP | Intuitionistic Metric Temporal Logic. | Luiz De S, Bernardo Toninho, Frank Pfenning |
| 2022 | ESOP | Polarized Subtyping. | Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning |
| 2022 | FSCD | Type-Based Termination for Futures. | Siva Somayyajula, Frank Pfenning |
| 2021 | Coordination | Manifestly Phased Communication via Shared Session Types. | Chuta Sano, Stephanie Balzer, Frank Pfenning |
| 2021 | ESOP | Nested Session Types. | Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning |
| 2021 | PPDP | A Decade of Dependent Session Types. | Bernardo Toninho, Lus Caires, Frank Pfenning |
| 2020 | CONCUR | Session Types with Arithmetic Refinements. | Ankush Das, Frank Pfenning |
| 2020 | FSCD | Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). | Ankush Das, Frank Pfenning |
| 2020 | FSCD | Semi-Axiomatic Sequent Calculus. | Henry DeYoung, Frank Pfenning, Klaas Pruiksma |
| 2020 | PPDP | Verified Linear Session-Typed Concurrent Programming. | Ankush Das, Frank Pfenning |
| 2019 | CONCUR | Domain-Aware Session Types. | Lus Caires, Jorge A. Prez, Frank Pfenning, Bernardo Toninho |
| 2019 | ESOP | Manifest Deadlock-Freedom for Shared Session Types. | Stephanie Balzer, Bernardo Toninho, Frank Pfenning |
| 2018 | CONCUR | A Universal Session Type for Untyped Asynchronous Communication. | Stephanie Balzer, Frank Pfenning, Bernardo Toninho |
| 2018 | ESOP | Session-Typed Concurrent Contracts. | Hannah Gommerstadt, Limin Jia, Frank Pfenning |
| 2018 | LICS | Work Analysis with Resource-Aware Session Types. | Ankush Das, Jan Hoffmann, Frank Pfenning |
| 2016 | APLAS | Substructural Proofs as Automata. | Henry DeYoung, Frank Pfenning |
| 2016 | POPL | Monitors and blame assignment for higher-order session types. | Limin Jia, Hannah Gommerstadt, Frank Pfenning |
| 2015 | FOSSACS | Polarized Substructural Session Types. | Frank Pfenning, Dennis Griffith |
| 2015 | POPL | Proof theory and its role in programming language research. | Frank Pfenning |
| 2013 | ESOP | Behavioral Polymorphism and Parametricity in Session-Based Communication. | Lus Caires, Jorge A. Prez, Frank Pfenning, Bernardo Toninho |
| 2013 | ESOP | Higher-Order Processes, Functions, and Sessions: A Monadic Integration. | Bernardo Toninho, Lus Caires, Frank Pfenning |
| 2012 | CSL | Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. | Henry DeYoung, Lus Caires, Frank Pfenning, Bernardo Toninho |
| 2012 | ESOP | Linear Logical Relations for Session-Based Concurrency. | Jorge A. Prez, Lus Caires, Frank Pfenning, Bernardo Toninho |
| 2012 | FOSSACS | Functions as Session-Typed Processes. | Bernardo Toninho, Lus Caires, Frank Pfenning |
| 2011 | CPP | Proof-Carrying Code in a Session-Typed Process Calculus. | Frank Pfenning, Lus Caires, Bernardo Toninho |
| 2011 | PPDP | Dependent session types via intuitionistic linear type theory. | Bernardo Toninho, Lus Caires, Frank Pfenning |
| 2010 | CONCUR | Session Types as Intuitionistic Linear Propositions. | Lus Caires, Frank Pfenning |
| 2010 | LICS | Possession as Linear Knowledge. | Frank Pfenning |
| 2010 | SP | A Proof-Carrying File System. | Deepak Garg, Frank Pfenning |
| 2009 | CADE | Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. | Sean McLaughlin, Frank Pfenning |
| 2009 | LICS | Substructural Operational Semantics as Ordered Logic Programming. | Frank Pfenning, Robert J. Simmons |
| 2009 | PEPM | Linear logical approximations. | Robert J. Simmons, Frank Pfenning |
| 2008 | ICALP | Linear Logical Algorithms. | Robert J. Simmons, Frank Pfenning |
| 2008 | LPAR | Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. | Sean McLaughlin, Frank Pfenning |
| 2007 | ICFP | Subtyping and intersection types revisited. | Frank Pfenning |
| 2007 | ICRA | Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. | Uluc Saranli, Frank Pfenning |
| 2007 | NDSS | Consumable Credentials in Linear-Logic-Based Access-Control Systems. | Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter |
| 2006 | CADE | A Logical Characterization of Forward and Backward Chaining in the Inverse Method. | Kaustuv Chaudhuri, Frank Pfenning, Greg Price |
| 2006 | ESORICS | A Linear Logic of Authorization and Knowledge. | Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter |
| 2005 | CADE | A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. | Kaustuv Chaudhuri, Frank Pfenning |
| 2005 | CONCUR | Type-Directed Concurrency. | Deepak Garg, Frank Pfenning |
| 2005 | CSL | Focusing the Inverse Method for Linear Logic. | Kaustuv Chaudhuri, Frank Pfenning |
| 2005 | ICFP | Towards a type theory of contexts. | Frank Pfenning |
| 2005 | POPL | A probabilistic language based upon sampling functions. | Sungwoo Park, Frank Pfenning, Sebastian Thrun |
| 2005 | PPDP | Monadic concurrent linear logic programming. | Pablo Lpez, Frank Pfenning, Jeff Polakow, Kevin Watkins |
| 2004 | APLAS | Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). | Frank Pfenning |
| 2004 | LICS | A Symmetric Modal Lambda Calculus for Distributed Computing. | Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning |
| 2004 | POPL | Tridirectional typechecking. | Jana Dunfield, Frank Pfenning |
| 2003 | CADE | Optimizing Higher-Order Pattern Unification. | Brigitte Pientka, Frank Pfenning |
| 2003 | FOSSACS | Type Assignment for Intersections and Unions in Call-by-Value Languages. | Jana Dunfield, Frank Pfenning |
| 2003 | ICFP | A modal foundation for meta-variables. | Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning |
| 2003 | IJCAI | A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data. | Sebastian Thrun, Geoffrey J. Gordon, Frank Pfenning, Mary Berna, Brennan Sellner, Brad Lisien |
| 2003 | POPL | A type theory for memory allocation and data layout. | Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning |
| 2001 | LICS | Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. | Frank Pfenning |
| 2000 | ICFP | Intersection types and computational effects. | Rowan Davies, Frank Pfenning |
| 2000 | PEPM | On the Logical Foundations of Staged Computation (Abstract of Invited Talk). | Frank Pfenning |
| 1999 | CADE | System Description: Twelf - A Meta-Logical Framework for Deductive Systems. | Frank Pfenning, Carsten Schrmann |
| 1999 | ICLP | The Relative Complement Problem for Higher-Order Patterns. | Alberto Momigliano, Frank Pfenning |
| 1999 | POPL | Dependent Types in Practical Programming. | Hongwei Xi, Frank Pfenning |
| 1999 | PPDP | Logical and Meta-Logical Frameworks (Abstract). | Frank Pfenning |
| 1998 | CADE | Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). | Frank Pfenning |
| 1998 | CADE | Automated Theorem Proving in a Simple Meta-Logic for LF. | Carsten Schrmann, Frank Pfenning |
| 1998 | PLDI | Run-time Code Generation and Modal-ML. | Philip Wickline, Peter Lee, Frank Pfenning |
| 1998 | PLDI | Eliminating Array Bound Checking Through Dependent Types. | Hongwei Xi, Frank Pfenning |
| 1997 | LICS | Linear Higher-Order Pre-Unification. | Iliano Cervesato, Frank Pfenning |
| 1996 | ESOP | Mode and Termination Checking for Higher-Order Logic Programs. | Ekkehard Rohwedder, Frank Pfenning |
| 1996 | ICLP | Unification via Explicit Substitutions: The Case of Higher-Order Patterns. | Gilles Dowek, Thrse Hardin, Claude Kirchner, Frank Pfenning |
| 1996 | LICS | A Linear Logical Framework. | Iliano Cervesato, Frank Pfenning |
| 1996 | POPL | A Modal Analysis of Staged Computation. | Rowan Davies, Frank Pfenning |
| 1995 | LICS | Structural Cut Elimination | Frank Pfenning |
| 1994 | CADE | Elf: A Meta-Language for Deductive Systems (System Descrition). | Frank Pfenning |
| 1993 | LICS | On the Unification Problem for Cartesian Closed Categories | Paliath Narendran, Frank Pfenning, Richard Statman |
| 1992 | CADE | Implementing the Meta-Theory of Deductive Systems. | Frank Pfenning, Ekkehard Rohwedder |
| 1992 | LICS | Compiler Verification in LF | John Hannan, Frank Pfenning |
| 1991 | LICS | Unification and Anti-Unification in the Calculus of Constructions | Frank Pfenning |
| 1991 | PEPM | Compiling the Polymorphic Lambda-Calculus. | Spiro Michaylov, Frank Pfenning |
| 1991 | PLDI | Refinement Types for ML. | Timothy S. Freeman, Frank Pfenning |
| 1990 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning |
| 1990 | CADE | Tutorial on Lambda-Prolog. | Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning |
| 1990 | CADE | Presenting Intuitive Deductions via Symmetric Simplification. | Frank Pfenning, Dan Nesmith |
| 1990 | ICLP | Types in Logic Programming. | Frank Pfenning |
| 1989 | ICML | Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. | Scott Dietzen, Frank Pfenning |
| 1989 | LICS | Elf: A Language for Logic Definition and Verified Metaprogramming | Frank Pfenning |
| 1989 | MFPS | Inductively Defined Types in the Calculus of Constructions. | Frank Pfenning, Christine Paulin-Mohring |
| 1988 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning |
| 1988 | CADE | Single Axioms in the Implicational Propositional Calculus. | Frank Pfenning |
| 1988 | PLDI | Higher-Order Abstract Syntax. | Frank Pfenning, Conal Elliott |
| 1986 | CADE | The TPS Theorem Proving System. | Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper |
| 1984 | CADE | Analytic and Non-analytic Proofs. | Frank Pfenning |