Frank Pfenning

According to our database, Frank Pfenning authored at least 178 papers between 1984 and 2024.

Collaborative distances:

• Dijkstra number of three.
• Erdős number of three.

2024

Parametric Subtyping for Structural Parametric Polymorphism.

Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das

Proc. ACM Program. Lang., January, 2024

Adjoint Natural Deduction (Extended Version).

Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka

CoRR, 2024

Adjoint Natural Deduction.

Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka

Proceedings of the 9th International Conference on Formal Structures for Computation and Deduction, 2024

Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax).

Adrian Francalanza, Gerard Tabone, Frank Pfenning

Proceedings of the Coordination Models and Languages, 2024

2023

A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns.

Zhibo Chen, Frank Pfenning

CoRR, 2023

Dependent Type Refinements for Futures.

Siva Somayyajula, Frank Pfenning

Proceedings of the 39th Conference on the Mathematical Foundations of Programming Semantics, 2023

Intuitionistic Metric Temporal Logic.

Luiz De Sá, Bernardo Toninho, Frank Pfenning

Proceedings of the International Symposium on Principles and Practice of Declarative Programming, 2023

A Logical Framework with Higher-Order Rational (Circular) Terms.

Zhibo Chen, Frank Pfenning

Proceedings of the Foundations of Software Science and Computation Structures, 2023

Relating Message Passing and Shared Memory, Proof-Theoretically.

Frank Pfenning, Klaas Pruiksma

Proceedings of the Coordination Models and Languages, 2023

2022

Nested Session Types.

Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning

ACM Trans. Program. Lang. Syst., 2022

Circular Proofs as Session-Typed Processes: A Local Validity Condition.

Farzaneh Derakhshan, Frank Pfenning

Log. Methods Comput. Sci., 2022

Rast: A Language for Resource-Aware Session Types.

Ankush Das, Frank Pfenning

Log. Methods Comput. Sci., 2022

Session-typed concurrent contracts.

Hannah Gommerstadt, Limin Jia, Frank Pfenning

J. Log. Algebraic Methods Program., 2022

Back to futures.

Klaas Pruiksma, Frank Pfenning

J. Funct. Program., 2022

Data Layout from a Type-Theoretic Perspective (extended version).

Henry DeYoung, Frank Pfenning

Proceedings of the 38th Conference on the Mathematical Foundations of Programming Semantics, 2022

Type-Based Termination for Futures.

Siva Somayyajula, Frank Pfenning

Proceedings of the 7th International Conference on Formal Structures for Computation and Deduction, 2022

Polarized Subtyping.

Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning

Proceedings of the Programming Languages and Systems, 2022

2021

A message-passing interpretation of adjoint logic.

Klaas Pruiksma, Frank Pfenning

J. Log. Algebraic Methods Program., 2021

Circular Proofs as Processes: Type-Based Termination via Arithmetic Refinements.

Siva Somayyajula, Frank Pfenning

CoRR, 2021

Subtyping on Nested Polymorphic Session Types.

Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning

CoRR, 2021

A Decade of Dependent Session Types.

Bernardo Toninho, Luís Caires, Frank Pfenning

Proceedings of the PPDP 2021: 23rd International Symposium on Principles and Practice of Declarative Programming, 2021

Resource-Aware Session Types for Digital Contracts.

Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

Manifestly Phased Communication via Shared Session Types.

Chuta Sano, Stephanie Balzer, Frank Pfenning

Proceedings of the Coordination Models and Languages, 2021

2020

Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points.

Farzaneh Derakhshan, Frank Pfenning

CoRR, 2020

Session Types with Arithmetic Refinements and Their Application to Work Analysis.

Ankush Das, Frank Pfenning

CoRR, 2020

Verified Linear Session-Typed Concurrent Programming.

Ankush Das, Frank Pfenning

Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

Semi-Axiomatic Sequent Calculus.

Henry DeYoung, Frank Pfenning, Klaas Pruiksma

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description).

Ankush Das, Frank Pfenning

Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Session Types with Arithmetic Refinements.

Ankush Das, Frank Pfenning

Proceedings of the 31st International Conference on Concurrency Theory, 2020

2019

Domain-Aware Session Types (Extended Version).

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

CoRR, 2019

Resource-Aware Session Types for Digital Contracts.

Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning

CoRR, 2019

Manifest Deadlock-Freedom for Shared Session Types.

Stephanie Balzer, Bernardo Toninho, Frank Pfenning

Proceedings of the Programming Languages and Systems, 2019

Domain-Aware Session Types.

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Proceedings of the 30th International Conference on Concurrency Theory, 2019

2018

Parallel complexity analysis with temporal session types.

Ankush Das, Jan Hoffmann, Frank Pfenning

Proc. ACM Program. Lang., 2018

Work Analysis with Resource-Aware Session Types.

Ankush Das, Jan Hoffmann, Frank Pfenning

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

A Universal Session Type for Untyped Asynchronous Communication.

Stephanie Balzer, Frank Pfenning, Bernardo Toninho

Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017

Manifest sharing with session types.

Stephanie Balzer, Frank Pfenning

Proc. ACM Program. Lang., 2017

2016

Linear logic propositions as session types.

Luís Caires, Frank Pfenning, Bernardo Toninho

Math. Struct. Comput. Sci., 2016

Design and Implementation of Concurrent C0.

Max Willsey, Rokhini Prabhu, Frank Pfenning

Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016

Non-Blocking Concurrent Imperative Programming with Session Types.

Miguel E. P. Silva, Mário Florido, Frank Pfenning

Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016

Intersections and Unions of Session Types.

Cosku Acay, Frank Pfenning

Proceedings of the Proceedings Eighth Workshop on Intersection Types and Related Systems, 2016

Monitors and blame assignment for higher-order session types.

Limin Jia, Hannah Gommerstadt, Frank Pfenning

Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Substructural Proofs as Automata.

Henry DeYoung, Frank Pfenning

Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015

Proof theory and its role in programming language research.

Frank Pfenning

Proceedings of the Programming Languages Mentoring Workshop, 2015

Polarized Substructural Session Types.

Frank Pfenning, Dennis Griffith

Proceedings of the Foundations of Software Science and Computation Structures, 2015

Objects as session-typed processes.

Stephanie Balzer, Frank Pfenning

Proceedings of the 5th International Workshop on Programming Based on Actors, 2015

2014

<i>Programming with Higher-Order Logic</i>, by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012, Hardcover, ISBN-10: 052187940X, xiv + 306 pp.

Frank Pfenning

Theory Pract. Log. Program., 2014

A Linear Logic Programming Language for Concurrent Programming over Graph Structures.

Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, Frank Pfenning

Theory Pract. Log. Program., 2014

Linear logical relations and observational equivalences for session-based concurrency.

Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho

Inf. Comput., 2014

Corecursion and Non-divergence in Session-Typed Processes.

Bernardo Toninho, Luís Caires, Frank Pfenning

Proceedings of the Trustworthy Global Computing - 9th International Symposium, 2014

2013

Higher-Order Processes, Functions, and Sessions: A Monadic Integration.

Bernardo Toninho, Luís Caires, Frank Pfenning

Proceedings of the Programming Languages and Systems, 2013

Behavioral Polymorphism and Parametricity in Session-Based Communication.

Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho

Proceedings of the Programming Languages and Systems, 2013

2012

Stateful authorization logic - Proof theory and a case study.

Deepak Garg, Frank Pfenning

J. Comput. Secur., 2012

Towards concurrent type theory.

Luís Caires, Frank Pfenning, Bernardo Toninho

Proceedings of the 8th ACM SIGPLAN Workshop on Types in Languages Design and Implementation, 2012

Functions as Session-Typed Processes.

Bernardo Toninho, Luís Caires, Frank Pfenning

Proceedings of the Foundations of Software Science and Computational Structures, 2012

Linear Logical Relations for Session-Based Concurrency.

Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho

Proceedings of the Programming Languages and Systems, 2012

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication.

Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho

Proceedings of the Computer Science Logic (CSL'12), 2012

2011

Logical approximation for program analysis.

Robert J. Simmons, Frank Pfenning

High. Order Symb. Comput., 2011

A Proof-Carrying File System with Revocable and Use-Once Certificates.

Jamie Morgenstern, Deepak Garg, Frank Pfenning

Proceedings of the Security and Trust Management - 7th International Workshop, 2011

Dependent session types via intuitionistic linear type theory.

Bernardo Toninho, Luís Caires, Frank Pfenning

Proceedings of the 13th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2011

Proof-Carrying Code in a Session-Typed Process Calculus.

Frank Pfenning, Luís Caires, Bernardo Toninho

Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010

Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance

William Lovas, Frank Pfenning

Log. Methods Comput. Sci., 2010

A Proof-Carrying File System.

Deepak Garg, Frank Pfenning

Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010

Possession as Linear Knowledge.

Frank Pfenning

Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility, 2010

Session Types as Intuitionistic Linear Propositions.

Luís Caires, Frank Pfenning

Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009

Refinement Types as Proof Irrelevance.

William Lovas, Frank Pfenning

Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

Linear logical approximations.

Robert J. Simmons, Frank Pfenning

Proceedings of the 2009 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-based Program Manipulation, 2009

Substructural Operational Semantics as Ordered Logic Programming.

Frank Pfenning, Robert J. Simmons

Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method.

Sean McLaughlin, Frank Pfenning

Proceedings of the Automated Deduction, 2009

2008

A probabilistic language based on sampling functions.

Sungwoo Park, Frank Pfenning, Sebastian Thrun

ACM Trans. Program. Lang. Syst., 2008

Contextual modal type theory.

Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka

ACM Trans. Comput. Log., 2008

A Logical Characterization of Forward and Backward Chaining in the Inverse Method.

Kaustuv Chaudhuri, Frank Pfenning, Greg Price

J. Autom. Reason., 2008

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic.

Sean McLaughlin, Frank Pfenning

Proceedings of the Logic for Programming, 2008

Linear Logical Algorithms.

Robert J. Simmons, Frank Pfenning

Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

An Authorization Logic With Explicit Time.

Henry DeYoung, Deepak Garg, Frank Pfenning

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

2007

Intuitionistic Letcc via Labelled Deduction.

Jason Reed, Frank Pfenning

Proceedings of the 5th Workshop on Methods for Modalities, 2007

A Bidirectional Refinement Type System for LF.

William Lovas, Frank Pfenning

Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2007

On a Logical Foundation for Explicit Substitutions.

Frank Pfenning

Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

Consumable Credentials in Linear-Logic-Based Access-Control Systems.

Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter

Proceedings of the Network and Distributed System Security Symposium, 2007

Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems.

Uluc Saranli, Frank Pfenning

Proceedings of the 2007 IEEE International Conference on Robotics and Automation, 2007

Subtyping and intersection types revisited.

Frank Pfenning

Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

2006

A Linear Logic of Authorization and Knowledge.

Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter

Proceedings of the Computer Security, 2006

Non-Interference in Constructive Authorization Logic.

Deepak Garg, Frank Pfenning

Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

2005

On equivalence and canonical forms in the LF type theory.

Robert Harper, Frank Pfenning

ACM Trans. Comput. Log., 2005

Staged computation with names and necessity.

Aleksandar Nanevski, Frank Pfenning

J. Funct. Program., 2005

A monadic analysis of information flow security with mutable state.

Karl Crary, Aleksey Kliger, Frank Pfenning

J. Funct. Program., 2005

Monadic concurrent linear logic programming.

Pablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins

Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2005

A probabilistic language based upon sampling functions.

Sungwoo Park, Frank Pfenning, Sebastian Thrun

Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Towards a type theory of contexts.

Frank Pfenning

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

Focusing the Inverse Method for Linear Logic.

Kaustuv Chaudhuri, Frank Pfenning

Proceedings of the Computer Science Logic, 19th International Workshop, 2005

Type-Directed Concurrency.

Deepak Garg, Frank Pfenning

Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.

Kaustuv Chaudhuri, Frank Pfenning

Proceedings of the Automated Deduction, 2005

2004

ETPS: A System to Help Students Write Formal Proofs.

Peter B. Andrews, Chad E. Brown, Frank Pfenning, Matthew Bishop, Sunil Issar, Hongwei Xi

J. Autom. Reason., 2004

Specifying Properties of Concurrent Computations in CLF.

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages, 2004

Verifying Uniqueness in a Logical Framework.

Penny Anderson, Frank Pfenning

Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

Tridirectional typechecking.

Jana Dunfield, Frank Pfenning

Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2004

A Symmetric Modal Lambda Calculus for Distributed Computing.

Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning

Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk).

Frank Pfenning

Proceedings of the Programming Languages and Systems: Second Asian Symposium, 2004

2003

Higher-order pattern complement and the strict lambda-calculus.

Alberto Momigliano, Frank Pfenning

ACM Trans. Comput. Log., 2003

Automated techniques for provably safe mobile code.

Christopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning

Theor. Comput. Sci., 2003

A Linear Spine Calculus.

Iliano Cervesato, Frank Pfenning

J. Log. Comput., 2003

A Concurrent Logical Framework: The Propositional Fragment.

Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker

Proceedings of the Types for Proofs and Programs, International Workshop, 2003

A Coverage Checking Algorithm for LF.

Carsten Schürmann, Frank Pfenning

Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

A type theory for memory allocation and data layout.

Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning

Proceedings of the Conference Record of POPL 2003: The 30th SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2003

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

Proceedings of the IJCAI-03, 2003

A modal foundation for meta-variables.

Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning

Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Type Assignment for Intersections and Unions in Call-by-Value Languages.

Jana Dunfield, Frank Pfenning

Proceedings of the Foundations of Software Science and Computational Structures, 2003

Optimizing Higher-Order Pattern Unification.

Brigitte Pientka, Frank Pfenning

Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002

Editorial.

Martín Abadi, Leonid Libkin, Frank Pfenning

ACM Trans. Comput. Log., 2002

A Linear Logical Framework.

Iliano Cervesato, Frank Pfenning

Inf. Comput., 2002

Invited talk: Tri-Directional Type Checking.

Frank Pfenning

Proceedings of the Intersection Types and Related Systems, 2002

Preface.

Frank Pfenning

Proceedings of the International Workshop on Logical Frameworks and Meta-Languages, 2002

Trustless Grid Computing in ConCert.

Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning

Proceedings of the Grid Computing, 2002

2001

Primitive recursion for higher-order abstract syntax.

Carsten Schürmann, Joëlle Despeyroux, Frank Pfenning

Theor. Comput. Sci., 2001

A judgmental reconstruction of modal logic.

Frank Pfenning, Rowan Davies

Math. Struct. Comput. Sci., 2001

A modal analysis of staged computation.

Rowan Davies, Frank Pfenning

J. ACM, 2001

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory.

Frank Pfenning

Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

Logical Frameworks.

Frank Pfenning

Proceedings of the Handbook of Automated Reasoning (in 2 volumes), 2001

2000

Efficient resource management for linear logic proof search.

Iliano Cervesato, Joshua S. Hodas, Frank Pfenning

Theor. Comput. Sci., 2000

Structural Cut Elimination: I. Intuitionistic and Classical Logic.

Frank Pfenning

Inf. Comput., 2000

Editorial: Strategies in Automated Deduction.

Bernhard Gramlich, Hélène Kirchner, Frank Pfenning

Ann. Math. Artif. Intell., 2000

Reasoning about Staged Computation.

Frank Pfenning

Proceedings of the Semantics, 2000

On the Logical Foundations of Staged Computation (Abstract of Invited Talk).

Frank Pfenning

Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '00), 2000

Intersection types and computational effects.

Rowan Davies, Frank Pfenning

Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 2000

1999

Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic.

J. Polokow, Frank Pfenning

Proceedings of the Fifteenth Conference on Mathematical Foundations of Progamming Semantics, 1999

On proving syntactic properties of CPS programs.

Olivier Danvy, Belmina Dzafic, Frank Pfenning

Proceedings of the Third Workshop on Higher-Order Operational Techniques in Semantics, 1999

Natural Deduction for Intuitionistic Non-communicative Linear Logic.

Jeff Polakow, Frank Pfenning

Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

Logical and Meta-Logical Frameworks (Abstract).

Frank Pfenning

Proceedings of the Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29, 1999

Dependent Types in Practical Programming.

Hongwei Xi, Frank Pfenning

Proceedings of the POPL '99, 1999

The Relative Complement Problem for Higher-Order Patterns.

Alberto Momigliano, Frank Pfenning

Proceedings of the Logic Programming: The 1999 International Conference, Las Cruces, New Mexico, USA, November 29, 1999

System Description: Twelf - A Meta-Logical Framework for Deductive Systems.

Frank Pfenning, Carsten Schürmann

Proceedings of the Automated Deduction, 1999

1998

Note by the Guest Editors.

Wilfried Sieg, Frank Pfenning

Stud Logica, 1998

A Module System for a Programming Language Based on the LF Logical Framework.

Robert Harper, Frank Pfenning

J. Log. Comput., 1998

Algorithms for Equality and Unification in the Presence of Notational Definitions.

Frank Pfenning, Carsten Schürmann

Proceedings of the Workshop on Proof Search in Type-Theoretic Languages (in conjunction with CADE-15 Conference), 1998

Modal Types as Staging Specifications for Run-Time Code Generation.

Philip Wickline, Peter Lee, Frank Pfenning, Rowan Davies

ACM Comput. Surv., 1998

Eliminating Array Bound Checking Through Dependent Types.

Hongwei Xi, Frank Pfenning

Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), 1998

Run-time Code Generation and Modal-ML.

Philip Wickline, Peter Lee, Frank Pfenning

Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), 1998

Automated Theorem Proving in a Simple Meta-Logic for LF.

Carsten Schürmann, Frank Pfenning

Proceedings of the Automated Deduction, 1998

Reasoning About Deductions in Linear Logic (Abstract of Invited Talk).

Frank Pfenning

Proceedings of the Automated Deduction, 1998

1997

On the Unification Problem for Cartesian Closed Categories.

Paliath Narendran, Frank Pfenning, Richard Statman

J. Symb. Log., 1997

Linear Higher-Order Pre-Unification.

Iliano Cervesato, Frank Pfenning

Proceedings of the Proceedings, 12th Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, June 29, 1997

1996

TPS: A Theorem-Proving System for Classical Type Theory.

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi

J. Autom. Reason., 1996

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.

Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning

Proceedings of the Logic Programming, 1996

Mode and Termination Checking for Higher-Order Logic Programs.

Ekkehard Rohwedder, Frank Pfenning

Proceedings of the Programming Languages and Systems, 1996

The Practice of Logical Frameworks.

Frank Pfenning

Proceedings of the Trees in Algebra and Programming, 1996

1995

On a modal lambda calculus for S4.

Frank Pfenning, Hao-Chi Wong

Proceedings of the Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, 1995

Structural Cut Elimination

Frank Pfenning

Proceedings of the Proceedings, 1995

1994

Elf: A Meta-Language for Deductive Systems (System Descrition).

Frank Pfenning

Proceedings of the Automated Deduction - CADE-12, 12th International Conference on Automated Deduction, Nancy, France, June 26, 1994

1993

On the Undecidability of Partial Polymorphic Type Reconstruction.

Frank Pfenning

Fundam. Informaticae, 1993

TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.

Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi

Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Unification in a Lambda-Calculus with Intersection Types.

Michael Kohlhase, Frank Pfenning

Proceedings of the Logic Programming, 1993

Higher-Order Logic Programming as Constraint Logic Programming.

Spiro Michaylov, Frank Pfenning

Proceedings of the Principles and Practice of Constraint Programming, 1993

1992

Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization.

Scott Dietzen, Frank Pfenning

Mach. Learn., 1992

Compiler Verification in LF

John Hannan, Frank Pfenning

Proceedings of the Seventh Annual Symposium on Logic in Computer Science (LICS '92), 1992

Implementing the Meta-Theory of Deductive Systems.

Frank Pfenning, Ekkehard Rohwedder

Proceedings of the Automated Deduction, 1992

Dependent Types in Logic Programming.

Frank Pfenning

Proceedings of the Types in Logic Programming., 1992

The Type System of a Higher-Order Logic Programming Language.

Gopalan Nadathur, Frank Pfenning

Proceedings of the Types in Logic Programming., 1992

1991

Metacircularity in the Polymorphic lambda-Calculus.

Frank Pfenning, Peter Lee

Theor. Comput. Sci., 1991

Uniform Proofs as a Foundation for Logic Programming.

Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov

Ann. Pure Appl. Log., 1991

A Declarative Alternative to "Assert" in Logic Programming.

Scott Dietzen, Frank Pfenning

Proceedings of the Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, Oct. 28, 1991

Refinement Types for ML.

Timothy S. Freeman, Frank Pfenning

Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), 1991

Compiling the Polymorphic Lambda-Calculus.

Spiro Michaylov, Frank Pfenning

Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 1991

Unification and Anti-Unification in the Calculus of Constructions

Frank Pfenning

Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Natural Semantics and Some of Its Meta-Theory in Elf.

Spiro Michaylov, Frank Pfenning

Proceedings of the Extensions of Logic Programming, Second International Workshop, 1991

1990

Types in Logic Programming.

Frank Pfenning

Proceedings of the Logic Programming, 1990

Presenting Intuitive Deductions via Symmetric Simplification.

Frank Pfenning, Dan Nesmith

Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on Lambda-Prolog.

Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning

Proceedings of the 10th International Conference on Automated Deduction, 1990

The TPS Theorem Proving System.

Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning

Proceedings of the 10th International Conference on Automated Deduction, 1990

1989

LEAP: A Language with Eval And Polymorphism.

Frank Pfenning, Peter Lee

Proceedings of the TAPSOFT'89: Proceedings of the International Joint Conference on Theory and Practice of Software Development, 1989

Inductively Defined Types in the Calculus of Constructions.

Frank Pfenning, Christine Paulin-Mohring

Proceedings of the Mathematical Foundations of Programming Semantics, 5th International Conference, Tulane University, New Orleans, Louisiana, USA, March 29, 1989

Elf: A Language for Logic Definition and Verified Metaprogramming

Frank Pfenning

Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1988

The Ergo Attribute System.

Robert L. Nord, Frank Pfenning

Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, 1988

The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments.

Peter Lee, Frank Pfenning, Gene Rollins, William L. Scherlis

Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, 1988

Higher-Order Abstract Syntax.

Frank Pfenning, Conal Elliott

Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), 1988

Partial Polymorphic Type Inference and Higher-Order Unification.

Frank Pfenning

Proceedings of the 1988 ACM Conference on LISP and Functional Programming, 1988

Single Axioms in the Implicational Propositional Calculus.

Frank Pfenning

Proceedings of the 9th International Conference on Automated Deduction, 1988

1986

The TPS Theorem Proving System.

Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper

Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1984

Analytic and Non-analytic Proofs.

Frank Pfenning

Proceedings of the 7th International Conference on Automated Deduction, 1984