default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDFrank Pfenning
Person information
- affiliation: Carnegie Mellon University, Pittsburgh, PA, USA
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
showing all ?? records
Journal Articles
- 2024
[j43]Henry DeYoung
, Andreia Mordido, Frank Pfenning, Ankush Das:
Parametric Subtyping for Structural Parametric Polymorphism. Proc. ACM Program. Lang. 8(POPL): 2700-2730 (2024)- 2022
- [j42]Klaas Pruiksma, Frank Pfenning:
Back to futures. J. Funct. Program. 32: e6 (2022) - [j41]Hannah Gommerstadt, Limin Jia, Frank Pfenning:
Session-typed concurrent contracts. J. Log. Algebraic Methods Program. 124: 100731 (2022) - [j40]Ankush Das, Frank Pfenning:
Rast: A Language for Resource-Aware Session Types. Log. Methods Comput. Sci. 18(1) (2022) - [j39]Farzaneh Derakhshan, Frank Pfenning:
Circular Proofs as Session-Typed Processes: A Local Validity Condition. Log. Methods Comput. Sci. 18(2) (2022) - [j38]Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Nested Session Types. ACM Trans. Program. Lang. Syst. 44(3): 19:1-19:45 (2022) - 2021
- [j37]Klaas Pruiksma, Frank Pfenning:
A message-passing interpretation of adjoint logic. J. Log. Algebraic Methods Program. 120: 100637 (2021) - 2018
- [j36]Ankush Das, Jan Hoffmann, Frank Pfenning:
Parallel complexity analysis with temporal session types. Proc. ACM Program. Lang. 2(ICFP): 91:1-91:30 (2018) - 2017
- [j35]Stephanie Balzer, Frank Pfenning:
Manifest sharing with session types. Proc. ACM Program. Lang. 1(ICFP): 37:1-37:29 (2017) - 2016
- [j34]Luís Caires, Frank Pfenning, Bernardo Toninho:
Linear logic propositions as session types. Math. Struct. Comput. Sci. 26(3): 367-423 (2016) - 2014
- [j33]Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho:
Linear logical relations and observational equivalences for session-based concurrency. Inf. Comput. 239: 254-302 (2014) - [j32]Frank Pfenning:
Programming with Higher-Order Logic, by Dale Miller and Gopalan Nadathur, Cambridge University Press, 2012, Hardcover, ISBN-10: 052187940X, xiv + 306 pp. Theory Pract. Log. Program. 14(2): 265-267 (2014) - [j31]Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, Frank Pfenning:
A Linear Logic Programming Language for Concurrent Programming over Graph Structures. Theory Pract. Log. Program. 14(4-5): 493-507 (2014) - 2012
- [j30]Deepak Garg, Frank Pfenning:
Stateful authorization logic - Proof theory and a case study. J. Comput. Secur. 20(4): 353-391 (2012) - 2011
- [j29]Robert J. Simmons, Frank Pfenning:
Logical approximation for program analysis. High. Order Symb. Comput. 24(1-2): 41-80 (2011) - 2010
- [j28]William Lovas, Frank Pfenning:
Refinement Types for Logical Frameworks and Their Interpretation as Proof Irrelevance. Log. Methods Comput. Sci. 6(4) (2010) - 2008
- [j27]Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. J. Autom. Reason. 40(2-3): 133-177 (2008) - [j26]Aleksandar Nanevski, Frank Pfenning, Brigitte Pientka:
Contextual modal type theory. ACM Trans. Comput. Log. 9(3): 23:1-23:49 (2008) - [j25]Sungwoo Park, Frank Pfenning, Sebastian Thrun:
A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1): 4:1-4:46 (2008) - 2005
- [j24]Karl Crary, Aleksey Kliger, Frank Pfenning:
A monadic analysis of information flow security with mutable state. J. Funct. Program. 15(2): 249-291 (2005) - [j23]Aleksandar Nanevski, Frank Pfenning:
Staged computation with names and necessity. J. Funct. Program. 15(5): 893-939 (2005) - [j22]Robert Harper, Frank Pfenning:
On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1): 61-101 (2005) - 2004
- [j21]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. Reason. 32(1): 75-92 (2004) - 2003
- [j20]Iliano Cervesato, Frank Pfenning:
A Linear Spine Calculus. J. Log. Comput. 13(5): 639-688 (2003) - [j19]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) - [j18]Alberto Momigliano, Frank Pfenning:
Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. 4(4): 493-529 (2003) - 2002
- [j17]Iliano Cervesato, Frank Pfenning:
A Linear Logical Framework. Inf. Comput. 179(1): 19-75 (2002) - [j16]Martín Abadi, Leonid Libkin, Frank Pfenning:
Editorial. ACM Trans. Comput. Log. 3(3): 335-335 (2002) - 2001
- [j15]Rowan Davies, Frank Pfenning:
A modal analysis of staged computation. J. ACM 48(3): 555-604 (2001) - [j14]Frank Pfenning, Rowan Davies:
A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4): 511-540 (2001) - [j13]Carsten Schürmann, Joëlle Despeyroux, Frank Pfenning:
Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1-2): 1-57 (2001) - 2000
- [j12]Bernhard Gramlich, Hélène Kirchner, Frank Pfenning:
Editorial: Strategies in Automated Deduction. Ann. Math. Artif. Intell. 29(1-4) (2000) - [j11]Frank Pfenning:
Structural Cut Elimination: I. Intuitionistic and Classical Logic. Inf. Comput. 157(1-2): 84-141 (2000) - [j10]Iliano Cervesato, Joshua S. Hodas, Frank Pfenning:
Efficient resource management for linear logic proof search. Theor. Comput. Sci. 232(1-2): 133-163 (2000) - 1998
- [j9]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) - [j8]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) - [j7]Wilfried Sieg, Frank Pfenning:
Note by the Guest Editors. Stud Logica 60(1): 1 (1998) - 1997
- [j6]Paliath Narendran, Frank Pfenning, Richard Statman:
On the Unification Problem for Cartesian Closed Categories. J. Symb. Log. 62(2): 636-647 (1997) - 1996
- [j5]Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, Hongwei Xi:
TPS: A Theorem-Proving System for Classical Type Theory. J. Autom. Reason. 16(3): 321-353 (1996) - 1993
- [j4]Frank Pfenning:
On the Undecidability of Partial Polymorphic Type Reconstruction. Fundam. Informaticae 19(1/2): 185-199 (1993) - 1992
- [j3]Scott Dietzen, Frank Pfenning:
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. Mach. Learn. 9: 23-55 (1992) - 1991
- [j2]Dale Miller, Gopalan Nadathur, Frank Pfenning, Andre Scedrov:
Uniform Proofs as a Foundation for Logic Programming. Ann. Pure Appl. Log. 51(1-2): 125-157 (1991) - [j1]Frank Pfenning, Peter Lee:
Metacircularity in the Polymorphic lambda-Calculus. Theor. Comput. Sci. 89(1): 137-159 (1991)
Conference and Workshop Papers
- 2024
- [c138]Adrian Francalanza, Gerard Tabone, Frank Pfenning:
Implementing a Message-Passing Interpretation of the Semi-Axiomatic Sequent Calculus (Sax). COORDINATION 2024: 295-313 - [c137]Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka:
Adjoint Natural Deduction. FSCD 2024: 15:1-15:23 - 2023
- [c136]Frank Pfenning, Klaas Pruiksma:
Relating Message Passing and Shared Memory, Proof-Theoretically. COORDINATION 2023: 3-27 - [c135]Zhibo Chen, Frank Pfenning:
A Logical Framework with Higher-Order Rational (Circular) Terms. FoSSaCS 2023: 68-88 - [c134]Luiz De Sá, Bernardo Toninho, Frank Pfenning:
Intuitionistic Metric Temporal Logic. PPDP 2023: 9:1-9:13 - [c133]Siva Somayyajula, Frank Pfenning:
Dependent Type Refinements for Futures. MFPS 2023 - 2022
- [c132]Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Polarized Subtyping. ESOP 2022: 431-461 - [c131]Siva Somayyajula, Frank Pfenning:
Type-Based Termination for Futures. FSCD 2022: 12:1-12:21 - [c130]Henry DeYoung, Frank Pfenning:
Data Layout from a Type-Theoretic Perspective (extended version). MFPS 2022 - 2021
- [c129]Chuta Sano, Stephanie Balzer, Frank Pfenning:
Manifestly Phased Communication via Shared Session Types. COORDINATION 2021: 23-40 - [c128]Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning, Ishani Santurkar:
Resource-Aware Session Types for Digital Contracts. CSF 2021: 1-16 - [c127]Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Nested Session Types. ESOP 2021: 178-206 - [c126]Bernardo Toninho, Luís Caires, Frank Pfenning:
A Decade of Dependent Session Types. PPDP 2021: 3:1-3:3 - 2020
- [c125]Ankush Das, Frank Pfenning:
Session Types with Arithmetic Refinements. CONCUR 2020: 13:1-13:18 - [c124]Henry DeYoung, Frank Pfenning, Klaas Pruiksma:
Semi-Axiomatic Sequent Calculus. FSCD 2020: 29:1-29:22 - [c123]Ankush Das, Frank Pfenning:
Rast: Resource-Aware Session Types with Arithmetic Refinements (System Description). FSCD 2020: 33:1-33:17 - [c122]Ankush Das, Frank Pfenning:
Verified Linear Session-Typed Concurrent Programming. PPDP 2020: 7:1-7:15 - 2019
- [c121]Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho:
Domain-Aware Session Types. CONCUR 2019: 39:1-39:17 - [c120]Stephanie Balzer, Bernardo Toninho, Frank Pfenning:
Manifest Deadlock-Freedom for Shared Session Types. ESOP 2019: 611-639 - [c119]Klaas Pruiksma, Frank Pfenning:
A Message-Passing Interpretation of Adjoint Logic. PLACES@ETAPS 2019: 60-79 - 2018
- [c118]Stephanie Balzer, Frank Pfenning, Bernardo Toninho:
A Universal Session Type for Untyped Asynchronous Communication. CONCUR 2018: 30:1-30:18 - [c117]Hannah Gommerstadt, Limin Jia, Frank Pfenning:
Session-Typed Concurrent Contracts. ESOP 2018: 771-798 - [c116]Ankush Das, Jan Hoffmann, Frank Pfenning:
Work Analysis with Resource-Aware Session Types. LICS 2018: 305-314 - 2016
- [c115]Henry DeYoung, Frank Pfenning:
Substructural Proofs as Automata. APLAS 2016: 3-22 - [c114]Limin Jia, Hannah Gommerstadt, Frank Pfenning:
Monitors and blame assignment for higher-order session types. POPL 2016: 582-594 - [c113]Cosku Acay, Frank Pfenning:
Intersections and Unions of Session Types. ITRS 2016: 4-19 - [c112]Miguel E. P. Silva, Mário Florido, Frank Pfenning:
Non-Blocking Concurrent Imperative Programming with Session Types. LINEARITY 2016: 64-72 - [c111]Max Willsey, Rokhini Prabhu, Frank Pfenning:
Design and Implementation of Concurrent C0. LINEARITY 2016: 73-82 - 2015
- [c110]Stephanie Balzer, Frank Pfenning:
Objects as session-typed processes. AGERE!@SPLASH 2015: 13-24 - [c109]Frank Pfenning, Dennis Griffith:
Polarized Substructural Session Types. FoSSaCS 2015: 3-22 - 2014
- [c108]Bernardo Toninho, Luís Caires, Frank Pfenning:
Corecursion and Non-divergence in Session-Typed Processes. TGC 2014: 159-175 - 2013
- [c107]Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho:
Behavioral Polymorphism and Parametricity in Session-Based Communication. ESOP 2013: 330-349 - [c106]Bernardo Toninho, Luís Caires, Frank Pfenning:
Higher-Order Processes, Functions, and Sessions: A Monadic Integration. ESOP 2013: 350-369 - 2012
- [c105]Henry DeYoung, Luís Caires, Frank Pfenning, Bernardo Toninho:
Cut Reduction in Linear Logic as Asynchronous Session-Typed Communication. CSL 2012: 228-242 - [c104]Jorge A. Pérez, Luís Caires, Frank Pfenning, Bernardo Toninho:
Linear Logical Relations for Session-Based Concurrency. ESOP 2012: 539-558 - [c103]Bernardo Toninho, Luís Caires, Frank Pfenning:
Functions as Session-Typed Processes. FoSSaCS 2012: 346-360 - [c102]Luís Caires, Frank Pfenning, Bernardo Toninho:
Towards concurrent type theory. TLDI 2012: 1-12 - 2011
- [c101]Frank Pfenning, Luís Caires, Bernardo Toninho:
Proof-Carrying Code in a Session-Typed Process Calculus. CPP 2011: 21-36 - [c100]Bernardo Toninho, Luís Caires, Frank Pfenning:
Dependent session types via intuitionistic linear type theory. PPDP 2011: 161-172 - [c99]Jamie Morgenstern, Deepak Garg, Frank Pfenning:
A Proof-Carrying File System with Revocable and Use-Once Certificates. STM 2011: 40-55 - 2010
- [c98]Luís Caires, Frank Pfenning:
Session Types as Intuitionistic Linear Propositions. CONCUR 2010: 222-236 - [c97]Frank Pfenning:
Possession as Linear Knowledge. LAM@LICS 2010: 1 - [c96]Deepak Garg, Frank Pfenning:
A Proof-Carrying File System. IEEE Symposium on Security and Privacy 2010: 349-364 - [c95]Deepak Garg, Frank Pfenning:
Stateful Authorization Logic: - Proof Theory and a Case Study. STM 2010: 210-225 - 2009
- [c94]Sean McLaughlin, Frank Pfenning:
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. CADE 2009: 230-244 - [c93]Frank Pfenning, Robert J. Simmons:
Substructural Operational Semantics as Ordered Logic Programming. LICS 2009: 101-110 - [c92]Robert J. Simmons, Frank Pfenning:
Linear logical approximations. PEPM 2009: 9-20 - [c91]William Lovas, Frank Pfenning:
Refinement Types as Proof Irrelevance. TLCA 2009: 157-171 - 2008
- [c90]Henry DeYoung, Deepak Garg, Frank Pfenning:
An Authorization Logic With Explicit Time. CSF 2008: 133-145 - [c89]Robert J. Simmons, Frank Pfenning:
Linear Logical Algorithms. ICALP (2) 2008: 336-347 - [c88]Sean McLaughlin, Frank Pfenning:
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. LPAR 2008: 174-181 - 2007
- [c87]Frank Pfenning:
Subtyping and intersection types revisited. ICFP 2007: 219 - [c86]Uluc Saranli, Frank Pfenning:
Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. ICRA 2007: 3705-3710 - [c85]Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter:
Consumable Credentials in Linear-Logic-Based Access-Control Systems. NDSS 2007 - [c84]Frank Pfenning:
On a Logical Foundation for Explicit Substitutions. RTA 2007: 19 - [c83]Frank Pfenning:
On a Logical Foundation for Explicit Substitutions. TLCA 2007: 1 - [c82]Jason Reed, Frank Pfenning:
Intuitionistic Letcc via Labelled Deduction. M4M 2007: 91-111 - [c81]William Lovas, Frank Pfenning:
A Bidirectional Refinement Type System for LF. LFMTP@CADE 2007: 113-128 - 2006
- [c80]Kaustuv Chaudhuri, Frank Pfenning, Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method. IJCAR 2006: 97-111 - [c79]Deepak Garg, Frank Pfenning:
Non-Interference in Constructive Authorization Logic. CSFW 2006: 283-296 - [c78]Deepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter:
A Linear Logic of Authorization and Knowledge. ESORICS 2006: 297-312 - 2005
- [c77]Kaustuv Chaudhuri, Frank Pfenning:
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. CADE 2005: 69-83 - [c76]Deepak Garg, Frank Pfenning:
Type-Directed Concurrency. CONCUR 2005: 6-20 - [c75]Kaustuv Chaudhuri, Frank Pfenning:
Focusing the Inverse Method for Linear Logic. CSL 2005: 200-215 - [c74]Frank Pfenning:
Towards a type theory of contexts. MERLIN 2005: 1 - [c73]Sungwoo Park, Frank Pfenning, Sebastian Thrun:
A probabilistic language based upon sampling functions. POPL 2005: 171-182 - [c72]Pablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins:
Monadic concurrent linear logic programming. PPDP 2005: 35-46 - 2004
- [c71]Frank Pfenning:
Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). APLAS 2004: 196 - [c70]Tom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning:
A Symmetric Modal Lambda Calculus for Distributed Computing. LICS 2004: 286-295 - [c69]Jana Dunfield, Frank Pfenning:
Tridirectional typechecking. POPL 2004: 281-292 - [c68]Penny Anderson, Frank Pfenning:
Verifying Uniqueness in a Logical Framework. TPHOLs 2004: 18-33 - [c67]Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker:
Specifying Properties of Concurrent Computations in CLF. LFM@IJCAR 2004: 67-87 - 2003
- [c66]Brigitte Pientka, Frank Pfenning:
Optimizing Higher-Order Pattern Unification. CADE 2003: 473-487 - [c65]Jana Dunfield, Frank Pfenning:
Type Assignment for Intersections and Unions in Call-by-Value Languages. FoSSaCS 2003: 250-266 - [c64]Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning:
A modal foundation for meta-variables. MERLIN 2003 - [c63]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 - [c62]Leaf Petersen, Robert Harper, Karl Crary, Frank Pfenning:
A type theory for memory allocation and data layout. POPL 2003: 172-184 - [c61]Carsten Schürmann, Frank Pfenning:
A Coverage Checking Algorithm for LF. TPHOLs 2003: 120-135 - [c60]Kevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker:
A Concurrent Logical Framework: The Propositional Fragment. TYPES 2003: 355-377 - 2002
- [c59]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 - [c58]Frank Pfenning:
Preface. LFM 2002: 146 - [c57]Frank Pfenning:
Invited talk: Tri-Directional Type Checking. ITRS 2002 - 2001
- [c56]Frank Pfenning:
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. LICS 2001: 221-230 - 2000
- [c55]Rowan Davies, Frank Pfenning:
Intersection types and computational effects. ICFP 2000: 198-208 - [c54]Frank Pfenning:
On the Logical Foundations of Staged Computation (Abstract of Invited Talk). PEPM 2000: 33 - [c53]Frank Pfenning:
Reasoning about Staged Computation. SAIG 2000: 5-6 - 1999
- [c52]Alberto Momigliano, Frank Pfenning:
The Relative Complement Problem for Higher-Order Patterns. APPIA-GULP-PRODE 1999: 497-512 - [c51]Frank Pfenning, Carsten Schürmann:
System Description: Twelf - A Meta-Logical Framework for Deductive Systems. CADE 1999: 202-206 - [c50]Alberto Momigliano, Frank Pfenning:
The Relative Complement Problem for Higher-Order Patterns. ICLP 1999: 380-394 - [c49]Hongwei Xi, Frank Pfenning:
Dependent Types in Practical Programming. POPL 1999: 214-227 - [c48]Frank Pfenning:
Logical and Meta-Logical Frameworks (Abstract). PPDP 1999: 206 - [c47]Jeff Polakow, Frank Pfenning:
Natural Deduction for Intuitionistic Non-communicative Linear Logic. TLCA 1999: 295-309 - [c46]Olivier Danvy, Belmina Dzafic, Frank Pfenning:
On proving syntactic properties of CPS programs. HOOTS 1999: 21-33 - [c45]J. Polokow, Frank Pfenning:
Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. MFPS 1999: 449-466 - 1998
- [c44]Frank Pfenning:
Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). CADE 1998: 1-2 - [c43]Carsten Schürmann, Frank Pfenning:
Automated Theorem Proving in a Simple Meta-Logic for LF. CADE 1998: 286-300 - [c42]Philip Wickline, Peter Lee, Frank Pfenning:
Run-time Code Generation and Modal-ML. PLDI 1998: 224-235 - [c41]Hongwei Xi, Frank Pfenning:
Eliminating Array Bound Checking Through Dependent Types. PLDI 1998: 249-257 - [c40]Frank Pfenning, Carsten Schürmann:
Algorithms for Equality and Unification in the Presence of Notational Definitions. TYPES 1998: 179-193 - [c39]Frank Pfenning, Carsten Schürmann:
Algorithms for Equality and Unification in the Presence of Notational Definitions. Proof Search in Type-Theoretic Languages@CADE 1998: 1-13 - 1997
- [c38]Iliano Cervesato, Frank Pfenning:
Linear Higher-Order Pre-Unification. LICS 1997: 422-433 - [c37]Joëlle Despeyroux, Frank Pfenning, Carsten Schürmann:
Primitive Recursion for Higher-Order Abstract Syntax. TLCA 1997: 147-163 - 1996
- [c36]Frank Pfenning:
The Practice of Logical Frameworks. CAAP 1996: 119-134 - [c35]Iliano Cervesato, Joshua S. Hodas, Frank Pfenning:
Efficient Resource Management for Linear Logic Proof Search. ELP 1996: 67-81 - [c34]Ekkehard Rohwedder, Frank Pfenning:
Mode and Termination Checking for Higher-Order Logic Programs. ESOP 1996: 296-310 - [c33]Gilles Dowek, Thérèse Hardin, Claude Kirchner, Frank Pfenning:
Unification via Explicit Substitutions: The Case of Higher-Order Patterns. JICSLP 1996: 259-273 - [c32]Iliano Cervesato, Frank Pfenning:
A Linear Logical Framework. LICS 1996: 264-275 - [c31]Rowan Davies, Frank Pfenning:
A Modal Analysis of Staged Computation. POPL 1996: 258-270 - 1995
- [c30]Frank Pfenning:
Structural Cut Elimination. LICS 1995: 156-166 - [c29]Frank Pfenning, Hao-Chi Wong:
On a modal lambda calculus for S4. MFPS 1995: 515-534 - 1994
- [c28]Frank Pfenning:
Elf: A Meta-Language for Deductive Systems (System Descrition). CADE 1994: 811-815 - 1993
- [c27]Paliath Narendran, Frank Pfenning, Richard Statman:
On the Unification Problem for Cartesian Closed Categories. LICS 1993: 57-63 - [c26]Spiro Michaylov, Frank Pfenning:
Higher-Order Logic Programming as Constraint Logic Programming. PPCP 1993: 210-218 - [c25]Michael Kohlhase, Frank Pfenning:
Unification in a Lambda-Calculus with Intersection Types. ILPS 1993: 488-505 - [c24]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 - 1992
- [c23]Frank Pfenning, Ekkehard Rohwedder:
Implementing the Meta-Theory of Deductive Systems. CADE 1992: 537-551 - [c22]John Hannan, Frank Pfenning:
Compiler Verification in LF. LICS 1992: 407-418 - 1991
- [c21]Spiro Michaylov, Frank Pfenning:
Natural Semantics and Some of Its Meta-Theory in Elf. ELP 1991: 299-344 - [c20]Frank Pfenning:
Unification and Anti-Unification in the Calculus of Constructions. LICS 1991: 74-85 - [c19]Spiro Michaylov, Frank Pfenning:
Compiling the Polymorphic Lambda-Calculus. PEPM 1991: 285-296 - [c18]Timothy S. Freeman, Frank Pfenning:
Refinement Types for ML. PLDI 1991: 268-277 - [c17]Scott Dietzen, Frank Pfenning:
A Declarative Alternative to "Assert" in Logic Programming. ISLP 1991: 372-386 - 1990
- [c16]Frank Pfenning, Dan Nesmith:
Presenting Intuitive Deductions via Symmetric Simplification. CADE 1990: 336-350 - [c15]Peter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning:
The TPS Theorem Proving System. CADE 1990: 641-642 - [c14]Amy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning:
Tutorial on Lambda-Prolog. CADE 1990: 682 - [c13]Frank Pfenning:
Types in Logic Programming. ICLP 1990: 786 - 1989
- [c12]Scott Dietzen, Frank Pfenning:
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. ML 1989: 447-449 - [c11]Frank Pfenning:
Elf: A Language for Logic Definition and Verified Metaprogramming. LICS 1989: 313-322 - [c10]Frank Pfenning, Christine Paulin-Mohring:
Inductively Defined Types in the Calculus of Constructions. Mathematical Foundations of Programming Semantics 1989: 209-228 - [c9]Frank Pfenning, Peter Lee:
LEAP: A Language with Eval And Polymorphism. TAPSOFT, Vol.2 1989: 345-359 - 1988
- [c8]Frank Pfenning:
Single Axioms in the Implicational Propositional Calculus. CADE 1988: 710-713 - [c7]Peter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning:
The TPS Theorem Proving System. CADE 1988: 760-761 - [c6]Frank Pfenning:
Partial Polymorphic Type Inference and Higher-Order Unification. LISP and Functional Programming 1988: 153-163 - [c5]Frank Pfenning, Conal Elliott:
Higher-Order Abstract Syntax. PLDI 1988: 199-208 - [c4]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 - [c3]Robert L. Nord, Frank Pfenning:
The Ergo Attribute System. Software Development Environments (SDE) 1988: 110-120 - 1986
- [c2]Peter B. Andrews, Frank Pfenning, Sunil Issar, Carl P. Klapper:
The TPS Theorem Proving System. CADE 1986: 663-664 - 1984
- [c1]Frank Pfenning:
Analytic and Non-analytic Proofs. CADE 1984: 394-413
Parts in Books or Collections
- 2001
- [p3]Frank Pfenning:
Logical Frameworks. Handbook of Automated Reasoning 2001: 1063-1147 - 1992
- [p2]Gopalan Nadathur, Frank Pfenning:
The Type System of a Higher-Order Logic Programming Language. Types in Logic Programming 1992: 245-283 - [p1]Frank Pfenning:
Dependent Types in Logic Programming. Types in Logic Programming 1992: 285-311
Editorship
- 2013
- [e8]Frank Pfenning:
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 [contents] - 2007
- [e7]Frank Pfenning:
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 [contents] - 2006
- [e6]Frank Pfenning:
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 [contents] - 2003
- [e5]Frank Pfenning, Yannis Smaragdakis:
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 [contents] - 2002
- [e4]Frank Pfenning:
International Workshop on Logical Frameworks and Meta-Languages, LFM 2002, FLoC Satellite Event, Copenhagen, Denmark, July 26, 2002. Electronic Notes in Theoretical Computer Science 70(2), Elsevier 2002 [contents] - 2000
- [e3]Maurizio Gabbrielli, Frank Pfenning:
Proceedings of the 2nd international ACM SIGPLAN conference on on Principles and practice of declarative programming, Montreal, Canada, September 20-23, 2000. ACM 2000, ISBN 1-58113-265-4 [contents] - 1994
- [e2]Frank Pfenning:
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 [contents] - 1992
- [e1]Frank Pfenning:
Types in Logic Programming. The MIT Press 1992, ISBN 0-262-16131-1, pp. 1-332 [contents]
Informal and Other Publications
- 2024
- [i23]Junyoung Jang, Sophia Roshal, Frank Pfenning, Brigitte Pientka:
Adjoint Natural Deduction (Extended Version). CoRR abs/2402.01428 (2024) - 2023
- [i22]Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das:
Parametric Subtyping for Structural Parametric Polymorphism. CoRR abs/2307.13661 (2023) - [i21]Zhibo Chen, Frank Pfenning:
A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns. CoRR abs/2312.07263 (2023) - 2022
- [i20]Zeeshan Lakhani, Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Polarized Subtyping. CoRR abs/2201.10998 (2022) - [i19]Zhibo Chen, Frank Pfenning:
A Logical Framework with Higher-Order Rational (Circular) Terms. CoRR abs/2210.06663 (2022) - 2021
- [i18]Chuta Sano, Stephanie Balzer, Frank Pfenning:
Manifestly Phased Communication via Shared Session Types. CoRR abs/2101.06249 (2021) - [i17]Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Subtyping on Nested Polymorphic Session Types. CoRR abs/2103.15193 (2021) - [i16]Siva Somayyajula, Frank Pfenning:
Circular Proofs as Processes: Type-Based Termination via Arithmetic Refinements. CoRR abs/2105.06024 (2021) - 2020
- [i15]Ankush Das, Frank Pfenning:
Session Types with Arithmetic Refinements and Their Application to Work Analysis. CoRR abs/2001.04439 (2020) - [i14]Farzaneh Derakhshan, Frank Pfenning:
Circular Proofs in First-Order Linear Logic with Least and Greatest Fixed Points. CoRR abs/2001.05132 (2020) - [i13]Klaas Pruiksma, Frank Pfenning:
Back to Futures. CoRR abs/2002.04607 (2020) - [i12]Ankush Das, Frank Pfenning:
Session Types with Arithmetic Refinements. CoRR abs/2005.05970 (2020) - [i11]Ankush Das, Henry DeYoung, Andreia Mordido, Frank Pfenning:
Nested Session Types. CoRR abs/2010.06482 (2020) - [i10]Ankush Das, Frank Pfenning:
Rast: A Language for Resource-Aware Session Types. CoRR abs/2012.13129 (2020) - 2019
- [i9]Ankush Das, Stephanie Balzer, Jan Hoffmann, Frank Pfenning:
Resource-Aware Session Types for Digital Contracts. CoRR abs/1902.06056 (2019) - [i8]Luís Caires, Jorge A. Pérez, Frank Pfenning, Bernardo Toninho:
Domain-Aware Session Types (Extended Version). CoRR abs/1907.01318 (2019) - [i7]Farzaneh Derakhshan, Frank Pfenning:
Circular Proofs as Session-Typed Processes: A Local Validity Condition. CoRR abs/1908.01909 (2019) - 2018
- [i6]Ankush Das, Jan Hoffmann, Frank Pfenning:
Parallel Complexity Analysis with Temporal Session Types. CoRR abs/1804.06013 (2018) - 2017
- [i5]Ankush Das, Jan Hoffmann, Frank Pfenning:
Work Analysis with Resource-Aware Session Types. CoRR abs/1712.08310 (2017) - 2015
- [i4]Frank Pfenning:
Proof theory and its role in programming language research. PLMW@POPL 2015: 4:1 - 2014
- [i3]Flávio Cruz, Ricardo Rocha, Seth Copen Goldstein, Frank Pfenning:
A Linear Logic Programming Language for Concurrent Programming over Graph Structures. CoRR abs/1405.3556 (2014) - 2001
- [i2]Alberto Momigliano, Frank Pfenning:
Higher-Order Pattern Complement and the Strict Lambda-Calculus. CoRR cs.LO/0109072 (2001) - [i1]Robert Harper, Frank Pfenning:
On Equivalence and Canonical Forms in the LF Type Theory. CoRR cs.LO/0110028 (2001)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from 
to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the 
of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from 
, 
, and 
to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from 
.
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-10-07 22:06 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated and maintained by:
the dblp computer science bibliography is funded and supported by:
