Frank Pfenning

According to our database1, Frank Pfenning authored at least 164 papers between 1984 and 2021.

Collaborative distances:

Awards

ACM Fellow

ACM Fellow 2015, "For contributions to the logical foundations of automatic theorem proving and types for programming languages.".

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

Online presence:

On csauthors.net:

Bibliography

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

Subtyping on Nested Polymorphic Session Types.
CoRR, 2021

Nested Session Types.
Proceedings of the Programming Languages and Systems, 2021

Manifestly Phased Communication via Shared Session Types.
Proceedings of the Coordination Models and Languages, 2021

2020
Rast: A Language for Resource-Aware Session Types.
CoRR, 2020

Back to Futures.
CoRR, 2020

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

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

Verified Linear Session-Typed Concurrent Programming.
Proceedings of the PPDP '20: 22nd International Symposium on Principles and Practice of Declarative Programming, 2020

Semi-Axiomatic Sequent Calculus.
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description).
Proceedings of the 5th International Conference on Formal Structures for Computation and Deduction, 2020

Session Types with Arithmetic Refinements.
Proceedings of the 31st International Conference on Concurrency Theory, 2020

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

Domain-Aware Session Types (Extended Version).
CoRR, 2019

A Message-Passing Interpretation of Adjoint Logic.
Proceedings of the Proceedings Programming Language Approaches to Concurrency- and Communication-cEntric Software, 2019

Resource-Aware Session Types for Digital Contracts.
CoRR, 2019

Manifest Deadlock-Freedom for Shared Session Types.
Proceedings of the Programming Languages and Systems, 2019

Domain-Aware Session Types.
Proceedings of the 30th International Conference on Concurrency Theory, 2019

2018
Parallel complexity analysis with temporal session types.
Proc. ACM Program. Lang., 2018

Work Analysis with Resource-Aware Session Types.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

Session-Typed Concurrent Contracts.
Proceedings of the Programming Languages and Systems, 2018

A Universal Session Type for Untyped Asynchronous Communication.
Proceedings of the 29th International Conference on Concurrency Theory, 2018

2017
Manifest sharing with session types.
Proc. ACM Program. Lang., 2017

2016
Linear logic propositions as session types.
Math. Struct. Comput. Sci., 2016

Design and Implementation of Concurrent C0.
Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016

Non-Blocking Concurrent Imperative Programming with Session Types.
Proceedings of the Proceedings Fourth International Workshop on Linearity, 2016

Intersections and Unions of Session Types.
Proceedings of the Proceedings Eighth Workshop on Intersection Types and Related Systems, 2016

Monitors and blame assignment for higher-order session types.
Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016

Substructural Proofs as Automata.
Proceedings of the Programming Languages and Systems - 14th Asian Symposium, 2016

2015
Proof theory and its role in programming language research.
Proceedings of the Programming Languages Mentoring Workshop, 2015

Polarized Substructural Session Types.
Proceedings of the Foundations of Software Science and Computation Structures, 2015

Objects as session-typed processes.
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.
Theory Pract. Log. Program., 2014

A Linear Logic Programming Language for Concurrent Programming over Graph Structures.
Theory Pract. Log. Program., 2014

Linear logical relations and observational equivalences for session-based concurrency.
Inf. Comput., 2014

Corecursion and Non-divergence in Session-Typed Processes.
Proceedings of the Trustworthy Global Computing - 9th International Symposium, 2014

2013
Higher-Order Processes, Functions, and Sessions: A Monadic Integration.
Proceedings of the Programming Languages and Systems, 2013

Behavioral Polymorphism and Parametricity in Session-Based Communication.
Proceedings of the Programming Languages and Systems, 2013

2012
Stateful authorization logic - Proof theory and a case study.
J. Comput. Secur., 2012

Towards concurrent type theory.
Proceedings of TLDI 2012: The Seventh ACM SIGPLAN Workshop on Types in Languages Design and Implementation, 2012

Functions as Session-Typed Processes.
Proceedings of the Foundations of Software Science and Computational Structures, 2012

Linear Logical Relations for Session-Based Concurrency.
Proceedings of the Programming Languages and Systems, 2012

Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication.
Proceedings of the Computer Science Logic (CSL'12), 2012

2011
Logical approximation for program analysis.
High. Order Symb. Comput., 2011

A Proof-Carrying File System with Revocable and Use-Once Certificates.
Proceedings of the Security and Trust Management - 7th International Workshop, 2011

Dependent session types via intuitionistic linear type theory.
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.
Proceedings of the Certified Programs and Proofs - First International Conference, 2011

2010
Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance
Log. Methods Comput. Sci., 2010

A Proof-Carrying File System.
Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010

Possession as Linear Knowledge.
Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility, 2010

Session Types as Intuitionistic Linear Propositions.
Proceedings of the CONCUR 2010 - Concurrency Theory, 21th International Conference, 2010

2009
Intuitionistic Letcc via Labelled Deduction.
Electron. Notes Theor. Comput. Sci., 2009

Refinement Types as Proof Irrelevance.
Proceedings of the Typed Lambda Calculi and Applications, 9th International Conference, 2009

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

Substructural Operational Semantics as Ordered Logic Programming.
Proceedings of the 24th Annual IEEE Symposium on Logic in Computer Science, 2009

Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method.
Proceedings of the Automated Deduction, 2009

2008
A probabilistic language based on sampling functions.
ACM Trans. Program. Lang. Syst., 2008

Contextual modal type theory.
ACM Trans. Comput. Log., 2008

A Logical Characterization of Forward and Backward Chaining in the Inverse Method.
J. Autom. Reason., 2008

Specifying Properties of Concurrent Computations in CLF.
Electron. Notes Theor. Comput. Sci., 2008

A Bidirectional Refinement Type System for LF.
Electron. Notes Theor. Comput. Sci., 2008

Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic.
Proceedings of the Logic for Programming, 2008

Linear Logical Algorithms.
Proceedings of the Automata, Languages and Programming, 35th International Colloquium, 2008

An Authorization Logic With Explicit Time.
Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

2007
On a Logical Foundation for Explicit Substitutions.
Proceedings of the Typed Lambda Calculi and Applications, 8th International Conference, 2007

Consumable Credentials in Linear-Logic-Based Access-Control Systems.
Proceedings of the Network and Distributed System Security Symposium, 2007

Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems.
Proceedings of the 2007 IEEE International Conference on Robotics and Automation, 2007

Subtyping and intersection types revisited.
Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, 2007

2006
A Linear Logic of Authorization and Knowledge.
Proceedings of the Computer Security, 2006

Non-Interference in Constructive Authorization Logic.
Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

2005
On equivalence and canonical forms in the LF type theory.
ACM Trans. Comput. Log., 2005

Staged computation with names and necessity.
J. Funct. Program., 2005

A monadic analysis of information flow security with mutable state.
J. Funct. Program., 2005

Monadic concurrent linear logic programming.
Proceedings of the 7th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, 2005

A probabilistic language based upon sampling functions.
Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005

Towards a type theory of contexts.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2005

Focusing the Inverse Method for Linear Logic.
Proceedings of the Computer Science Logic, 19th International Workshop, 2005

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

A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.
Proceedings of the Automated Deduction, 2005

2004
ETPS: A System to Help Students Write Formal Proofs.
J. Autom. Reason., 2004

Verifying Uniqueness in a Logical Framework.
Proceedings of the Theorem Proving in Higher Order Logics, 17th International Conference, 2004

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

A Symmetric Modal Lambda Calculus for Distributed Computing.
Proceedings of the 19th IEEE Symposium on Logic in Computer Science (LICS 2004), 2004

Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk).
Proceedings of the Programming Languages and Systems: Second Asian Symposium, 2004

2003
Higher-order pattern complement and the strict lambda-calculus.
ACM Trans. Comput. Log., 2003

Automated techniques for provably safe mobile code.
Theor. Comput. Sci., 2003

A Linear Spine Calculus.
J. Log. Comput., 2003

A Concurrent Logical Framework: The Propositional Fragment.
Proceedings of the Types for Proofs and Programs, International Workshop, 2003

A Coverage Checking Algorithm for LF.
Proceedings of the Theorem Proving in Higher Order Logics, 16th International Conference, 2003

A type theory for memory allocation and data layout.
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.
Proceedings of the IJCAI-03, 2003

A modal foundation for meta-variables.
Proceedings of the Eighth ACM SIGPLAN International Conference on Functional Programming, 2003

Type Assignment for Intersections and Unions in Call-by-Value Languages.
Proceedings of the Foundations of Software Science and Computational Structures, 2003

Optimizing Higher-Order Pattern Unification.
Proceedings of the Automated Deduction - CADE-19, 19th International Conference on Automated Deduction Miami Beach, FL, USA, July 28, 2003

2002
Editorial.
ACM Trans. Comput. Log., 2002

A Linear Logical Framework.
Inf. Comput., 2002

Invited talk: Tri-Directional Type Checking.
Electron. Notes Theor. Comput. Sci., 2002

Preface.
Electron. Notes Theor. Comput. Sci., 2002

Trustless Grid Computing in ConCert.
Proceedings of the Grid Computing, 2002

2001
Primitive recursion for higher-order abstract syntax.
Theor. Comput. Sci., 2001

A judgmental reconstruction of modal logic.
Math. Struct. Comput. Sci., 2001

A modal analysis of staged computation.
J. ACM, 2001

Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory.
Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, 2001

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

2000
Efficient resource management for linear logic proof search.
Theor. Comput. Sci., 2000

Structural Cut Elimination: I. Intuitionistic and Classical Logic.
Inf. Comput., 2000

Editorial: Strategies in Automated Deduction.
Ann. Math. Artif. Intell., 2000

Reasoning about Staged Computation.
Proceedings of the Semantics, 2000

On the Logical Foundations of Staged Computation (Abstract of Invited Talk).
Proceedings of the 2000 ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM '00), 2000

Intersection types and computational effects.
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.
Proceedings of the Fifteenth Conference on Mathematical Foundations of Progamming Semantics, 1999

On proving syntactic properties of CPS programs.
Electron. Notes Theor. Comput. Sci., 1999

Natural Deduction for Intuitionistic Non-communicative Linear Logic.
Proceedings of the Typed Lambda Calculi and Applications, 4th International Conference, 1999

Logical and Meta-Logical Frameworks (Abstract).
Proceedings of the Principles and Practice of Declarative Programming, International Conference PPDP'99, Paris, France, September 29, 1999

Dependent Types in Practical Programming.
Proceedings of the POPL '99, 1999

System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
Proceedings of the Automated Deduction, 1999

The Relative Complement Problem for Higher-Order Patterns.
Proceedings of the 1999 Joint Conference on Declarative Programming, 1999

1998
Note by the Guest Editors.
Stud Logica, 1998

A Module System for a Programming Language Based on the LF Logical Framework.
J. Log. Comput., 1998

Algorithms for Equality and Unification in the Presence of Notational Definitions.
Electron. Notes Theor. Comput. Sci., 1998

Modal Types as Staging Specifications for Run-Time Code Generation.
ACM Comput. Surv., 1998

Eliminating Array Bound Checking Through Dependent Types.
Proceedings of the ACM SIGPLAN '98 Conference on Programming Language Design and Implementation (PLDI), 1998

Run-time Code Generation and Modal-ML.
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.
Proceedings of the Automated Deduction, 1998

Reasoning About Deductions in Linear Logic (Abstract of Invited Talk).
Proceedings of the Automated Deduction, 1998

1997
On the Unification Problem for Cartesian Closed Categories.
J. Symb. Log., 1997

Linear Higher-Order Pre-Unification.
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.
J. Autom. Reason., 1996

Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
Proceedings of the Logic Programming, 1996

Mode and Termination Checking for Higher-Order Logic Programs.
Proceedings of the Programming Languages and Systems, 1996

The Practice of Logical Frameworks.
Proceedings of the Trees in Algebra and Programming, 1996

1995
On a modal lambda calculus for S4.
Proceedings of the Eleventh Annual Conference on Mathematical Foundations of Programming Semantics, 1995

Structural Cut Elimination
Proceedings of the Proceedings, 1995

1994
Elf: A Meta-Language for Deductive Systems (System Descrition).
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.
Fundam. Informaticae, 1993

TPS: An Interactive and Automatic Tool for Proving Theorems of Type Theory.
Proceedings of the Higher Order Logic Theorem Proving and its Applications, 1993

Unification in a Lambda-Calculus with Intersection Types.
Proceedings of the Logic Programming, 1993

Higher-Order Logic Programming as Constraint Logic Programming.
Proceedings of the Principles and Practice of Constraint Programming, 1993

1992
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization.
Mach. Learn., 1992

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

Implementing the Meta-Theory of Deductive Systems.
Proceedings of the Automated Deduction, 1992

Dependent Types in Logic Programming.
Proceedings of the Types in Logic Programming., 1992

The Type System of a Higher-Order Logic Programming Language.
Proceedings of the Types in Logic Programming., 1992

1991
Metacircularity in the Polymorphic lambda-Calculus.
Theor. Comput. Sci., 1991

Uniform Proofs as a Foundation for Logic Programming.
Ann. Pure Appl. Log., 1991

A Declarative Alternative to "Assert" in Logic Programming.
Proceedings of the Logic Programming, Proceedings of the 1991 International Symposium, San Diego, California, USA, Oct. 28, 1991

Refinement Types for ML.
Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI), 1991

Compiling the Polymorphic Lambda-Calculus.
Proceedings of the Symposium on Partial Evaluation and Semantics-Based Program Manipulation, 1991

Unification and Anti-Unification in the Calculus of Constructions
Proceedings of the Sixth Annual Symposium on Logic in Computer Science (LICS '91), 1991

Natural Semantics and Some of Its Meta-Theory in Elf.
Proceedings of the Extensions of Logic Programming, Second International Workshop, 1991

1990
Types in Logic Programming.
Proceedings of the Logic Programming, 1990

Presenting Intuitive Deductions via Symmetric Simplification.
Proceedings of the 10th International Conference on Automated Deduction, 1990

Tutorial on Lambda-Prolog.
Proceedings of the 10th International Conference on Automated Deduction, 1990

1989
LEAP: A Language with Eval And Polymorphism.
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.
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
Proceedings of the Fourth Annual Symposium on Logic in Computer Science (LICS '89), 1989

1988
The Ergo Attribute System.
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.
Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, 1988

Higher-Order Abstract Syntax.
Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), 1988

Partial Polymorphic Type Inference and Higher-Order Unification.
Proceedings of the 1988 ACM Conference on LISP and Functional Programming, 1988

Single Axioms in the Implicational Propositional Calculus.
Proceedings of the 9th International Conference on Automated Deduction, 1988

The TPS Theorem Proving System.
Proceedings of the 9th International Conference on Automated Deduction, 1988

1986
The TPS Theorem Proving System.
Proceedings of the 8th International Conference on Automated Deduction, Oxford, England, July 27, 1986

1984
Analytic and Non-analytic Proofs.
Proceedings of the 7th International Conference on Automated Deduction, 1984


  Loading...