Frank Pfenning

221 papers A* 25A 30B 30C 13Journal 69Unranked 48

Year	Rank	Type	Title / Venue / Authors
2026	J	`jnl`	Grits: A message-passing programming language based on the semi-axiomatic sequent calculus. Sci. Comput. Program. Adrian Francalanza, Gerard Tabone, Frank Pfenning
2026	J	`jnl`	Security Reasoning via Substructural Dependency Tracking. Proc. ACM Program. Lang. Hemant Gouni, Frank Pfenning, Jonathan Aldrich
2025	J	`jnl`	A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns. ACM Trans. Comput. Log. Zhibo Chen, Frank Pfenning
2025	—	`conf`	CoLF Logic Programming as Infinitary Proof Exploration. LFMTP@FSCD Zhibo Chen, Frank Pfenning
2025	J	`jnl`	Structural Information Flow: A Fresh Look at Types for Non-interference. Proc. ACM Program. Lang. Hemant Gouni, Frank Pfenning, Jonathan Aldrich
2025	B	`conf`	Substructural Parametricity. FSCD C. B. Aberlé, Karl Crary, Chris Martens, Frank Pfenning
2025	J	`jnl`	Substructural Parametricity. CoRR C. B. Aberlé, Chris Martens, Frank Pfenning
2024	J	`jnl`	Adjoint Natural Deduction (Extended Version). CoRR Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
2024	B	`conf`	Adjoint Natural Deduction. FSCD Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka
2024	C	`conf`	Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax). COORDINATION Adrian Francalanza, Gerard Tabone, Frank Pfenning
2024	J	`jnl`	Parametric Subtyping for Structural Parametric Polymorphism. Proc. ACM Program. Lang. Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das
2023	B	`conf`	A Logical Framework with Higher-Order Rational (Circular) Terms. FoSSaCS Zhibo Chen, Frank Pfenning
2023	J	`jnl`	A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns. CoRR Zhibo Chen, Frank Pfenning
2023	B	`conf`	Dependent Type Refinements for Futures. MFPS Siva Somayyajula, Frank Pfenning
2023	C	`conf`	Intuitionistic Metric Temporal Logic. PPDP Luiz De Sá, Bernardo Toninho, Frank Pfenning
2023	J	`jnl`	Parametric Subtyping for Structural Parametric Polymorphism. CoRR Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das
2023	C	`conf`	Relating Message Passing and Shared Memory, Proof-Theoretically. COORDINATION Frank Pfenning, Klaas Pruiksma
2022	J	`jnl`	A Logical Framework with Higher-Order Rational (Circular) Terms. CoRR Zhibo Chen, Frank Pfenning
2022	J	`jnl`	Back to futures. J. Funct. Program. Klaas Pruiksma, Frank Pfenning
2022	J	`jnl`	Circular Proofs as Session-Typed Processes: A Local Validity Condition. Log. Methods Comput. Sci. Farzaneh Derakhshan, Frank Pfenning
2022	B	`conf`	Data Layout from a Type-Theoretic Perspective (extended version). MFPS Henry DeYoung, Frank Pfenning
2022	J	`jnl`	Nested Session Types. ACM Trans. Program. Lang. Syst. Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2022	A	`conf`	Polarized Subtyping. ESOP Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2022	J	`jnl`	Polarized Subtyping. CoRR Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2022	J	`jnl`	Rast: A Language for Resource-Aware Session Types. Log. Methods Comput. Sci. Ankush Das, Frank Pfenning
2022	J	`jnl`	Session-typed concurrent contracts. J. Log. Algebraic Methods Program. Hannah Gommerstadt, Limin Jia, Frank Pfenning
2022	B	`conf`	Type-Based Termination for Futures. FSCD Siva Somayyajula, Frank Pfenning
2021	C	`conf`	A Decade of Dependent Session Types. PPDP Bernardo Toninho, Luís Caires, Frank Pfenning
2021	J	`jnl`	A message-passing interpretation of adjoint logic. J. Log. Algebraic Methods Program. Klaas Pruiksma, Frank Pfenning
2021	J	`jnl`	Circular Proofs as Processes: Type-Based Termination via Arithmetic Refinements. CoRR Siva Somayyajula, Frank Pfenning
2021	C	`conf`	Manifestly Phased Communication via Shared Session Types. COORDINATION Chuta Sano, Stephanie Balzer, Frank Pfenning
2021	J	`jnl`	Manifestly Phased Communication via Shared Session Types. CoRR Chuta Sano, Stephanie Balzer, Frank Pfenning
2021	A	`conf`	Nested Session Types. ESOP Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2021	A	`conf`	Resource-Aware Session Types for Digital Contracts. CSF Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar
2021	J	`jnl`	Subtyping on Nested Polymorphic Session Types. CoRR Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2020	J	`jnl`	Back to Futures. CoRR Klaas Pruiksma, Frank Pfenning
2020	J	`jnl`	Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points. CoRR Farzaneh Derakhshan, Frank Pfenning
2020	J	`jnl`	Nested Session Types. CoRR Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning
2020	J	`jnl`	Rast: A Language for Resource-Aware Session Types. CoRR Ankush Das, Frank Pfenning
2020	B	`conf`	Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). FSCD Ankush Das, Frank Pfenning
2020	B	`conf`	Semi-Axiomatic Sequent Calculus. FSCD Henry DeYoung, Frank Pfenning, Klaas Pruiksma
2020	J	`jnl`	Session Types with Arithmetic Refinements and Their Application to Work Analysis. CoRR Ankush Das, Frank Pfenning
2020	B	`conf`	Session Types with Arithmetic Refinements. CONCUR Ankush Das, Frank Pfenning
2020	J	`jnl`	Session Types with Arithmetic Refinements. CoRR Ankush Das, Frank Pfenning
2020	C	`conf`	Verified Linear Session-Typed Concurrent Programming. PPDP Ankush Das, Frank Pfenning
2019	—	`conf`	A Message-Passing Interpretation of Adjoint Logic. PLACES@ETAPS Klaas Pruiksma, Frank Pfenning
2019	J	`jnl`	Circular Proofs as Session-Typed Processes: A Local Validity Condition. CoRR Farzaneh Derakhshan, Frank Pfenning
2019	J	`jnl`	Domain-Aware Session Types (Extended Version). CoRR Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho
2019	B	`conf`	Domain-Aware Session Types. CONCUR Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho
2019	A	`conf`	Manifest Deadlock-Freedom for Shared Session Types. ESOP Stephanie Balzer, Bernardo Toninho, Frank Pfenning
2019	J	`jnl`	Resource-Aware Session Types for Digital Contracts. CoRR Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning
2018	B	`conf`	A Universal Session Type for Untyped Asynchronous Communication. CONCUR Stephanie Balzer, Frank Pfenning, Bernardo Toninho
2018	J	`jnl`	Parallel Complexity Analysis with Temporal Session Types. CoRR Ankush Das, Jan Hoffmann, Frank Pfenning
2018	J	`jnl`	Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. Ankush Das, Jan Hoffmann, Frank Pfenning
2018	A	`conf`	Session-Typed Concurrent Contracts. ESOP Hannah Gommerstadt, Limin Jia, Frank Pfenning
2018	A*	`conf`	Work Analysis with Resource-Aware Session Types. LICS Ankush Das, Jan Hoffmann, Frank Pfenning
2017	J	`jnl`	Manifest sharing with session types. Proc. ACM Program. Lang. Stephanie Balzer, Frank Pfenning
2017	J	`jnl`	Work Analysis with Resource-Aware Session Types. CoRR Ankush Das, Jan Hoffmann, Frank Pfenning
2016	—	`conf`	Design and Implementation of Concurrent C0. LINEARITY Max Willsey, Rokhini Prabhu, Frank Pfenning
2016	—	`conf`	Intersections and Unions of Session Types. ITRS Cosku Acay, Frank Pfenning
2016	J	`jnl`	Linear logic propositions as session types. Math. Struct. Comput. Sci. Luís Caires, Frank Pfenning, Bernardo Toninho
2016	A*	`conf`	Monitors and blame assignment for higher-order session types. POPL Limin Jia, Hannah Gommerstadt, Frank Pfenning
2016	—	`conf`	Non-Blocking Concurrent Imperative Programming with Session Types. LINEARITY Miguel E. P. Silva, Mário Florido, Frank Pfenning
2016	B	`conf`	Substructural Proofs as Automata. APLAS Henry DeYoung, Frank Pfenning
2015	—	`conf`	Objects as session-typed processes. AGERE!@SPLASH Stephanie Balzer, Frank Pfenning
2015	B	`conf`	Polarized Substructural Session Types. FoSSaCS Frank Pfenning, Dennis Griffith
2015	—	`conf`	Proof theory and its role in programming language research. PLMW@POPL Frank Pfenning
2014	J	`jnl`	A Linear Logic Programming Language for Concurrent Programming over Graph Structures. CoRR Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, Frank Pfenning
2014	J	`jnl`	A Linear Logic Programming Language for Concurrent Programming over Graph Structures. Theory Pract. Log. Program. Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, Frank Pfenning
2014	—	`conf`	Corecursion and Non-divergence in Session-Typed Processes. TGC Bernardo Toninho, Luís Caires, Frank Pfenning
2014	J	`jnl`	Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput. Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho
2013	A	`conf`	Behavioral Polymorphism and Parametricity in Session-Based Communication. ESOP Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho
2013	B	`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 FoSSaCS Frank Pfenning
2013	A	`conf`	Higher-Order Processes, Functions, and Sessions: A Monadic Integration. ESOP Bernardo Toninho, Luís Caires, Frank Pfenning
2012	B	`conf`	Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. CSL Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho
2012	B	`conf`	Functions as Session-Typed Processes. FoSSaCS Bernardo Toninho, Luís Caires, Frank Pfenning
2012	A	`conf`	Linear Logical Relations for Session-Based Concurrency. ESOP Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho
2012	J	`jnl`	Stateful authorization logic - Proof theory and a case study. J. Comput. Secur. Deepak Garg, Frank Pfenning
2012	—	`conf`	Towards concurrent type theory. TLDI Luís Caires, Frank Pfenning, Bernardo Toninho
2011	—	`conf`	A Proof-Carrying File System with Revocable and Use-Once Certificates. STM Jamie Morgenstern, Deepak Garg, Frank Pfenning
2011	C	`conf`	Dependent session types via intuitionistic linear type theory. PPDP Bernardo Toninho, Luís Caires, Frank Pfenning
2011	J	`jnl`	Logical approximation for program analysis. High. Order Symb. Comput. Robert J. Simmons, Frank Pfenning
2011	B	`conf`	Proof-Carrying Code in a Session-Typed Process Calculus. CPP Frank Pfenning, Luís Caires, Bernardo Toninho
2010	A*	`conf`	A Proof-Carrying File System. IEEE Symposium on Security and Privacy Deepak Garg, Frank Pfenning
2010	—	`conf`	Possession as Linear Knowledge. LAM@LICS Frank Pfenning
2010	J	`jnl`	Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance Log. Methods Comput. Sci. William Lovas, Frank Pfenning
2010	B	`conf`	Session Types as Intuitionistic Linear Propositions. CONCUR Luís Caires, Frank Pfenning
2010	—	`conf`	Stateful Authorization Logic: - Proof Theory and a Case Study. STM Deepak Garg, Frank Pfenning
2009	A	`conf`	Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. CADE Sean McLaughlin, Frank Pfenning
2009	C	`conf`	Linear logical approximations. PEPM Robert J. Simmons, Frank Pfenning
2009	—	`conf`	Refinement Types as Proof Irrelevance. TLCA William Lovas, Frank Pfenning
2009	A*	`conf`	Substructural Operational Semantics as Ordered Logic Programming. LICS Frank Pfenning, Robert J. Simmons
2008	J	`jnl`	A Logical Characterization of Forward and Backward Chaining in the Inverse Method. J. Autom. Reason. Kaustuv Chaudhuri, Frank Pfenning, Greg Price
2008	J	`jnl`	A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. Sungwoo Park, Frank Pfenning, Sebastian Thrun
2008	A	`conf`	An Authorization Logic With Explicit Time. CSF Henry DeYoung, Deepak Garg, Frank Pfenning
2008	J	`jnl`	Contextual modal type theory. ACM Trans. Comput. Log. Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka
2008	B	`conf`	Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. LPAR Sean McLaughlin, Frank Pfenning
2008	—	`conf`	Linear Logical Algorithms. ICALP (2) Robert J. Simmons, Frank Pfenning
2007	—	`conf`	A Bidirectional Refinement Type System for LF. LFMTP@CADE William Lovas, Frank Pfenning
2007	A	`ed.`	Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings CADE Frank Pfenning
2007	A*	`conf`	Consumable Credentials in Linear-Logic-Based Access-Control Systems. NDSS Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter
2007	—	`conf`	Intuitionistic Letcc via Labelled Deduction. M4M Jason Reed, Frank Pfenning
2007	—	`conf`	On a Logical Foundation for Explicit Substitutions. RTA Frank Pfenning
2007	—	`conf`	On a Logical Foundation for Explicit Substitutions. TLCA Frank Pfenning
2007	A	`conf`	Subtyping and intersection types revisited. ICFP Frank Pfenning
2007	A*	`conf`	Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. ICRA Uluc Saranli, Frank Pfenning
2006	A	`conf`	A Linear Logic of Authorization and Knowledge. ESORICS Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter
2006	A	`conf`	A Logical Characterization of Forward and Backward Chaining in the Inverse Method. IJCAR Kaustuv Chaudhuri, Frank Pfenning, Greg Price
2006	—	`conf`	Non-Interference in Constructive Authorization Logic. CSFW Deepak Garg, Frank Pfenning
2006	—	`ed.`	Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings RTA Frank Pfenning
2005	A	`conf`	A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. CADE Kaustuv Chaudhuri, Frank Pfenning
2005	J	`jnl`	A monadic analysis of information flow security with mutable state. J. Funct. Program. Karl Crary, Aleksey Kliger, Frank Pfenning
2005	A*	`conf`	A probabilistic language based upon sampling functions. POPL Sungwoo Park, Frank Pfenning, Sebastian Thrun
2005	B	`conf`	Focusing the Inverse Method for Linear Logic. CSL Kaustuv Chaudhuri, Frank Pfenning
2005	C	`conf`	Monadic concurrent linear logic programming. PPDP Pablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins
2005	J	`jnl`	On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. Robert Harper, Frank Pfenning
2005	J	`jnl`	Staged computation with names and necessity. J. Funct. Program. Aleksandar Nanevski, Frank Pfenning
2005	—	`conf`	Towards a type theory of contexts. MERLIN Frank Pfenning
2005	B	`conf`	Type-Directed Concurrency. CONCUR Deepak Garg, Frank Pfenning
2004	A*	`conf`	A Symmetric Modal Lambda Calculus for Distributed Computing. LICS Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning
2004	J	`jnl`	ETPS: A System to Help Students Write Formal Proofs. J. Autom. Reason. Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi
2004	—	`conf`	Specifying Properties of Concurrent Computations in CLF. LFM@IJCAR Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker
2004	B	`conf`	Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). APLAS Frank Pfenning
2004	A*	`conf`	Tridirectional typechecking. POPL Jana Dunfield, Frank Pfenning
2004	—	`conf`	Verifying Uniqueness in a Logical Framework. TPHOLs Penny Anderson, Frank Pfenning
2003	—	`conf`	A Concurrent Logical Framework: The Propositional Fragment. TYPES Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker
2003	—	`conf`	A Coverage Checking Algorithm for LF. TPHOLs Carsten Schürmann, Frank Pfenning
2003	A*	`conf`	A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled Data. IJCAI Sebastian Thrun, Geoffrey J. Gordon, Frank Pfenning, Mary Berna, Brennan Sellner, Brad Lisien
2003	J	`jnl`	A Linear Spine Calculus. J. Log. Comput. Iliano Cervesato, Frank Pfenning
2003	—	`conf`	A modal foundation for meta-variables. MERLIN Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning
2003	A*	`conf`	A type theory for memory allocation and data layout. POPL Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning
2003	J	`jnl`	Automated techniques for provably safe mobile code. Theor. Comput. Sci. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning
2003	B	`ed.`	Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings GPCE Frank Pfenning, Yannis Smaragdakis
2003	J	`jnl`	Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. Alberto Momigliano, Frank Pfenning
2003	A	`conf`	Optimizing Higher-Order Pattern Unification. CADE Brigitte Pientka, Frank Pfenning
2003	B	`conf`	Type Assignment for Intersections and Unions in Call-by-Value Languages. FoSSaCS Jana Dunfield, Frank Pfenning
2002	J	`jnl`	A Linear Logical Framework. Inf. Comput. Iliano Cervesato, Frank Pfenning
2002	J	`jnl`	Editorial. ACM Trans. Comput. Log. Martín Abadi, Leonid Libkin, Frank Pfenning
2002	—	`ed.`	International Workshop on Logical Frameworks and Meta-Languages, LFM 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002 LFM Frank Pfenning
2002	—	`conf`	Invited talk: Tri-Directional Type Checking. ITRS Frank Pfenning
2002	—	`conf`	Preface. LFM Frank Pfenning
2002	—	`conf`	Trustless Grid Computing in ConCert. GRID Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning
2001	J	`jnl`	A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. Frank Pfenning, Rowan Davies
2001	J	`jnl`	A modal analysis of staged computation. J. ACM Rowan Davies, Frank Pfenning
2001	J	`jnl`	Higher-Order Pattern Complement and the Strict Lambda-Calculus CoRR Alberto Momigliano, Frank Pfenning
2001	A*	`conf`	Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. LICS Frank Pfenning
2001	—	`ch.`	Logical Frameworks. Handbook of Automated Reasoning Frank Pfenning
2001	J	`jnl`	On Equivalence and Canonical Forms in the LF Type Theory CoRR Robert Harper, Frank Pfenning
2001	J	`jnl`	Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. Carsten Schürmann, Joëlle Despeyroux, Frank Pfenning
2000	J	`jnl`	Editorial: Strategies in Automated Deduction. Ann. Math. Artif. Intell. Bernhard Gramlich, Hélène Kirchner, Frank Pfenning
2000	J	`jnl`	Efficient resource management for linear logic proof search. Theor. Comput. Sci. Iliano Cervesato, Joshua S. Hodas, Frank Pfenning
2000	A	`conf`	Intersection types and computational effects. ICFP Rowan Davies, Frank Pfenning
2000	C	`conf`	On the Logical Foundations of Staged Computation (Abstract of Invited Talk). PEPM Frank Pfenning
2000	C	`ed.`	Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000 PPDP Maurizio Gabbrielli, Frank Pfenning
2000	—	`conf`	Reasoning about Staged Computation. SAIG Frank Pfenning
2000	J	`jnl`	Structural Cut Elimination: I. Intuitionistic and Classical Logic. Inf. Comput. Frank Pfenning
1999	A*	`conf`	Dependent Types in Practical Programming. POPL Hongwei Xi, Frank Pfenning
1999	C	`conf`	Logical and Meta-Logical Frameworks (Abstract). PPDP Frank Pfenning
1999	—	`conf`	Natural Deduction for Intuitionistic Non-communicative Linear Logic. TLCA Jeff Polakow, Frank Pfenning
1999	—	`conf`	On proving syntactic properties of CPS programs. HOOTS Olivier Danvy, Belmina Dzafic, Frank Pfenning
1999	B	`conf`	Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. MFPS J. Polokow, Frank Pfenning
1999	A	`conf`	System Description: Twelf - A Meta-Logical Framework for Deductive Systems. CADE Frank Pfenning, Carsten Schürmann
1999	—	`conf`	The Relative Complement Problem for Higher-Order Patterns. APPIA-GULP-PRODE Alberto Momigliano, Frank Pfenning
1999	B	`conf`	The Relative Complement Problem for Higher-Order Patterns. ICLP Alberto Momigliano, Frank Pfenning
1998	J	`jnl`	A Module System for a Programming Language Based on the LF Logical Framework. J. Log. Comput. Robert Harper, Frank Pfenning
1998	—	`conf`	Algorithms for Equality and Unification in the Presence of Notational Definitions. TYPES Frank Pfenning, Carsten Schürmann
1998	—	`conf`	Algorithms for Equality and Unification in the Presence of Notational Definitions. Proof Search in Type-Theoretic Languages@CADE Frank Pfenning, Carsten Schürmann
1998	A	`conf`	Automated Theorem Proving in a Simple Meta-Logic for LF. CADE Carsten Schürmann, Frank Pfenning
1998	A*	`conf`	Eliminating Array Bound Checking Through Dependent Types. PLDI Hongwei Xi, Frank Pfenning
1998	J	`jnl`	Modal Types as Staging Specifications for Run-Time Code Generation. ACM Comput. Surv. Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies
1998	J	`jnl`	Note by the Guest Editors. Stud Logica Wilfried Sieg, Frank Pfenning
1998	A	`conf`	Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). CADE Frank Pfenning
1998	A*	`conf`	Run-time Code Generation and Modal-ML. PLDI Philip Wickline, Peter Lee, Frank Pfenning
1997	A*	`conf`	Linear Higher-Order Pre-Unification. LICS Iliano Cervesato, Frank Pfenning
1997	J	`jnl`	On the Unification Problem for Cartesian Closed Categories. J. Symb. Log. Paliath Narendran, Frank Pfenning, Richard Statman
1997	—	`conf`	Primitive Recursion for Higher-Order Abstract Syntax. TLCA Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann
1996	A*	`conf`	A Linear Logical Framework. LICS Iliano Cervesato, Frank Pfenning
1996	A*	`conf`	A Modal Analysis of Staged Computation. POPL Rowan Davies, Frank Pfenning
1996	—	`conf`	Efficient Resource Management for Linear Logic Proof Search. ELP Iliano Cervesato, Joshua S. Hodas, Frank Pfenning
1996	A	`conf`	Mode and Termination Checking for Higher-Order Logic Programs. ESOP Ekkehard Rohwedder, Frank Pfenning
1996	J	`jnl`	TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reason. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
1996	—	`conf`	The Practice of Logical Frameworks. CAAP Frank Pfenning
1996	—	`conf`	Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning
1995	B	`conf`	On a modal lambda calculus for S4. MFPS Frank Pfenning, Hao-Chi Wong
1995	A*	`conf`	Structural Cut Elimination LICS Frank Pfenning
1994	A	`conf`	Elf: A Meta-Language for Deductive Systems (System Descrition). CADE Frank Pfenning
1994	B	`ed.`	Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings LPAR Frank Pfenning
1993	—	`conf`	Higher-Order Logic Programming as Constraint Logic Programming. PPCP Spiro Michaylov, Frank Pfenning
1993	J	`jnl`	On the Undecidability of Partial Polymorphic Type Reconstruction. Fundam. Informaticae Frank Pfenning
1993	A*	`conf`	On the Unification Problem for Cartesian Closed Categories LICS Paliath Narendran, Frank Pfenning, Richard Statman
1993	—	`conf`	TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory. HUG Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi
1993	—	`conf`	Unification in a Lambda-Calculus with Intersection Types. ILPS Michael Kohlhase, Frank Pfenning
1992	A*	`conf`	Compiler Verification in LF LICS John Hannan, Frank Pfenning
1992	—	`ch.`	Dependent Types in Logic Programming. Types in Logic Programming Frank Pfenning
1992	J	`jnl`	Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. Mach. Learn. Scott Dietzen, Frank Pfenning
1992	A	`conf`	Implementing the Meta-Theory of Deductive Systems. CADE Frank Pfenning, Ekkehard Rohwedder
1992	—	`ch.`	The Type System of a Higher-Order Logic Programming Language. Types in Logic Programming Gopalan Nadathur, Frank Pfenning
1992	—	`book`	Types in Logic Programming. Frank Pfenning
1991	—	`conf`	A Declarative Alternative to "Assert" in Logic Programming. ISLP Scott Dietzen, Frank Pfenning
1991	C	`conf`	Compiling the Polymorphic Lambda-Calculus. PEPM Spiro Michaylov, Frank Pfenning
1991	J	`jnl`	Metacircularity in the Polymorphic lambda-Calculus. Theor. Comput. Sci. Frank Pfenning, Peter Lee
1991	—	`conf`	Natural Semantics and Some of Its Meta-Theory in Elf. ELP Spiro Michaylov, Frank Pfenning
1991	A*	`conf`	Refinement Types for ML. PLDI Timothy S. Freeman, Frank Pfenning
1991	A*	`conf`	Unification and Anti-Unification in the Calculus of Constructions LICS Frank Pfenning
1991	J	`jnl`	Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Log. Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov
1990	A	`conf`	Presenting Intuitive Deductions via Symmetric Simplification. CADE Frank Pfenning, Dan Nesmith
1990	A	`conf`	The TPS Theorem Proving System. CADE Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning
1990	A	`conf`	Tutorial on Lambda-Prolog. CADE Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning
1990	B	`conf`	Types in Logic Programming. ICLP Frank Pfenning
1989	A*	`conf`	Elf: A Language for Logic Definition and Verified Metaprogramming LICS Frank Pfenning
1989	—	`conf`	Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. ML Scott Dietzen, Frank Pfenning
1989	B	`conf`	Inductively Defined Types in the Calculus of Constructions. Mathematical Foundations of Programming Semantics Frank Pfenning, Christine Paulin-Mohring
1989	—	`conf`	LEAP: A Language with Eval And Polymorphism. TAPSOFT, Vol.2 Frank Pfenning, Peter Lee
1988	A*	`conf`	Higher-Order Abstract Syntax. PLDI Frank Pfenning, Conal Elliott
1988	—	`conf`	Partial Polymorphic Type Inference and Higher-Order Unification. LISP and Functional Programming Frank Pfenning
1988	A	`conf`	Single Axioms in the Implicational Propositional Calculus. CADE Frank Pfenning
1988	—	`conf`	The Ergo Attribute System. Software Development Environments (SDE) Robert L. Nord, Frank Pfenning
1988	—	`conf`	The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments. Software Development Environments (SDE) Peter Lee, Frank Pfenning, Gene Rollins, William L. Scherlis
1988	A	`conf`	The TPS Theorem Proving System. CADE Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning
1986	A	`conf`	The TPS Theorem Proving System. CADE Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper
1984	A	`conf`	Analytic and Non-analytic Proofs. CADE Frank Pfenning