Search the dblp DataBase
Frank Pfenning :
[Publications ]
[Author Rank by year ]
[Co-authors ]
[Prefers ]
[Cites ]
[Cited by ]
Publications of Author
Dale Miller , Gopalan Nadathur , Frank Pfenning , Andre Scedrov Uniform Proofs as a Foundation for Logic Programming. [Citation Graph (1, 0)][DBLP ] Ann. Pure Appl. Logic, 1991, v:51, n:1-2, pp:125-157 [Journal ] Alberto Momigliano , Frank Pfenning The Relative Complement Problem for Higher-Order Patterns. [Citation Graph (0, 0)][DBLP ] APPIA-GULP-PRODE, 1999, pp:497-512 [Conf ] Frank Pfenning Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). [Citation Graph (0, 0)][DBLP ] APLAS, 2004, pp:196- [Conf ] Frank Pfenning The Practice of Logical Frameworks. [Citation Graph (0, 0)][DBLP ] CAAP, 1996, pp:119-134 [Conf ] Peter B. Andrews , Sunil Issar , Daniel Nesmith , Frank Pfenning The TPS Theorem Proving System. [Citation Graph (0, 0)][DBLP ] CADE, 1988, pp:760-761 [Conf ] Peter B. Andrews , Sunil Issar , Dan Nesmith , Frank Pfenning The TPS Theorem Proving System. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:641-642 [Conf ] Peter B. Andrews , Frank Pfenning , Sunil Issar , C. P. Klapper The TPS Theorem Proving System. [Citation Graph (0, 0)][DBLP ] CADE, 1986, pp:663-664 [Conf ] Kaustuv Chaudhuri , Frank Pfenning A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. [Citation Graph (0, 0)][DBLP ] CADE, 2005, pp:69-83 [Conf ] Kaustuv Chaudhuri , Frank Pfenning , Greg Price A Logical Characterization of Forward and Backward Chaining in the Inverse Method. [Citation Graph (0, 0)][DBLP ] IJCAR, 2006, pp:97-111 [Conf ] Amy P. Felty , Elsa L. Gunter , Dale Miller , Frank Pfenning Tutorial on Lambda-Prolog. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:682- [Conf ] Frank Pfenning Analytic and Non-analytic Proofs. [Citation Graph (0, 0)][DBLP ] CADE, 1984, pp:394-413 [Conf ] Frank Pfenning Single Axioms in the Implicational Propositional Calculus. [Citation Graph (0, 0)][DBLP ] CADE, 1988, pp:710-713 [Conf ] Frank Pfenning Elf: A Meta-Language for Deductive Systems (System Descrition). [Citation Graph (0, 0)][DBLP ] CADE, 1994, pp:811-815 [Conf ] Frank Pfenning Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). [Citation Graph (0, 0)][DBLP ] CADE, 1998, pp:1-2 [Conf ] Frank Pfenning , Dan Nesmith Presenting Intuitive Deductions via Symmetric Simplification. [Citation Graph (0, 0)][DBLP ] CADE, 1990, pp:336-350 [Conf ] Frank Pfenning , Ekkehard Rohwedder Implementing the Meta-Theory of Deductive Systems. [Citation Graph (0, 0)][DBLP ] CADE, 1992, pp:537-551 [Conf ] Frank Pfenning , Carsten Schürmann System Description: Twelf - A Meta-Logical Framework for Deductive Systems. [Citation Graph (0, 0)][DBLP ] CADE, 1999, pp:202-206 [Conf ] Brigitte Pientka , Frank Pfenning Optimizing Higher-Order Pattern Unification. [Citation Graph (0, 0)][DBLP ] CADE, 2003, pp:473-487 [Conf ] Carsten Schürmann , Frank Pfenning Automated Theorem Proving in a Simple Meta-Logic for LF. [Citation Graph (0, 0)][DBLP ] CADE, 1998, pp:286-300 [Conf ] Deepak Garg , Frank Pfenning Type-Directed Concurrency. [Citation Graph (0, 0)][DBLP ] CONCUR, 2005, pp:6-20 [Conf ] Deepak Garg , Frank Pfenning Non-Interference in Constructive Authorization Logic. [Citation Graph (0, 0)][DBLP ] CSFW, 2006, pp:283-296 [Conf ] Kaustuv Chaudhuri , Frank Pfenning Focusing the Inverse Method for Linear Logic. [Citation Graph (0, 0)][DBLP ] CSL, 2005, pp:200-215 [Conf ] Spiro Michaylov , Frank Pfenning Natural Semantics and Some of Its Meta-Theory in Elf. [Citation Graph (0, 0)][DBLP ] ELP, 1991, pp:299-344 [Conf ] Iliano Cervesato , Joshua S. Hodas , Frank Pfenning Efficient Resource Management for Linear Logic Proof Search. [Citation Graph (0, 0)][DBLP ] ELP, 1996, pp:67-81 [Conf ] Ekkehard Rohwedder , Frank Pfenning Mode and Termination Checking for Higher-Order Logic Programs. [Citation Graph (0, 0)][DBLP ] ESOP, 1996, pp:296-310 [Conf ] Deepak Garg , Lujo Bauer , Kevin D. Bowers , Frank Pfenning , Michael K. Reiter A Linear Logic of Authorization and Knowledge. [Citation Graph (0, 0)][DBLP ] ESORICS, 2006, pp:297-312 [Conf ] Joshua Dunfield , Frank Pfenning Type Assignment for Intersections and Unions in Call-by-Value Languages. [Citation Graph (0, 0)][DBLP ] FoSSaCS, 2003, pp:250-266 [Conf ] Bor-Yuh Evan Chang , Karl Crary , Margaret DeLap , Robert Harper , Jason Liszka , Tom Murphy VII , Frank Pfenning Trustless Grid Computing in ConCert. [Citation Graph (0, 0)][DBLP ] GRID, 2002, pp:112-125 [Conf ] Rowan Davies , Frank Pfenning Intersection types and computational effects. [Citation Graph (0, 0)][DBLP ] ICFP, 2000, pp:198-208 [Conf ] Aleksandar Nanevski , Brigitte Pientka , Frank Pfenning A modal foundation for meta-variables. [Citation Graph (0, 0)][DBLP ] MERLIN, 2003, pp:- [Conf ] Gilles Dowek , Thérèse Hardin , Claude Kirchner , Frank Pfenning Unification via Explicit Substitutions: The Case of Higher-Order Patterns. [Citation Graph (0, 0)][DBLP ] JICSLP, 1996, pp:259-273 [Conf ] Alberto Momigliano , Frank Pfenning The Relative Complement Problem for Higher-Order Patterns. [Citation Graph (0, 0)][DBLP ] ICLP, 1999, pp:380-394 [Conf ] Frank Pfenning Types in Logic Programming. [Citation Graph (0, 0)][DBLP ] ICLP, 1990, pp:786- [Conf ] Scott Dietzen , Frank Pfenning Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. [Citation Graph (0, 0)][DBLP ] ML, 1989, pp:447-449 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] IJCAI, 2003, pp:1427-1428 [Conf ] Frank Pfenning Partial Polymorphic Type Inference and Higher-Order Unification. [Citation Graph (0, 0)][DBLP ] LISP and Functional Programming, 1988, pp:153-163 [Conf ] Iliano Cervesato , Frank Pfenning A Linear Logical Framework. [Citation Graph (0, 0)][DBLP ] LICS, 1996, pp:264-275 [Conf ] Iliano Cervesato , Frank Pfenning Linear Higher-Order Pre-Unification. [Citation Graph (0, 0)][DBLP ] LICS, 1997, pp:422-433 [Conf ] Frank Pfenning Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory. [Citation Graph (0, 0)][DBLP ] LICS, 2001, pp:- [Conf ] Frank Pfenning Elf: A Language for Logic Definition and Verified Metaprogramming [Citation Graph (0, 0)][DBLP ] LICS, 1989, pp:313-322 [Conf ] Frank Pfenning Unification and Anti-Unification in the Calculus of Constructions [Citation Graph (0, 0)][DBLP ] LICS, 1991, pp:74-85 [Conf ] Frank Pfenning Structural Cut Elimination [Citation Graph (0, 0)][DBLP ] LICS, 1995, pp:156-166 [Conf ] John Hannan , Frank Pfenning Compiler Verification in LF [Citation Graph (0, 0)][DBLP ] LICS, 1992, pp:407-418 [Conf ] Paliath Narendran , Frank Pfenning , Richard Statman On the Unification Problem for Cartesian Closed Categories [Citation Graph (0, 0)][DBLP ] LICS, 1993, pp:57-63 [Conf ] Tom Murphy VII , Karl Crary , Robert Harper , Frank Pfenning A Symmetric Modal Lambda Calculus for Distributed Computing. [Citation Graph (0, 0)][DBLP ] LICS, 2004, pp:286-295 [Conf ] Frank Pfenning , Christine Paulin-Mohring Inductively Defined Types in the Calculus of Constructions. [Citation Graph (0, 0)][DBLP ] Mathematical Foundations of Programming Semantics, 1989, pp:209-228 [Conf ] Spiro Michaylov , Frank Pfenning Compiling the Polymorphic Lambda-Calculus. [Citation Graph (0, 0)][DBLP ] PEPM, 1991, pp:285-296 [Conf ] Frank Pfenning On the Logical Foundations of Staged Computation (Abstract of Invited Talk). [Citation Graph (0, 0)][DBLP ] PEPM, 2000, pp:33- [Conf ] Hongwei Xi , Frank Pfenning Eliminating Array Bound Checking Through Dependent Types. [Citation Graph (0, 0)][DBLP ] PLDI, 1998, pp:249-257 [Conf ] Tim Freeman , Frank Pfenning Refinement Types for ML. [Citation Graph (0, 0)][DBLP ] PLDI, 1991, pp:268-277 [Conf ] Frank Pfenning , Conal Elliott Higher-Order Abstract Syntax. [Citation Graph (0, 0)][DBLP ] PLDI, 1988, pp:199-208 [Conf ] Philip Wickline , Peter Lee , Frank Pfenning Run-time Code Generation and Modal-ML. [Citation Graph (0, 0)][DBLP ] PLDI, 1998, pp:224-235 [Conf ] Rowan Davies , Frank Pfenning A Modal Analysis of Staged Computation. [Citation Graph (0, 0)][DBLP ] POPL, 1996, pp:258-270 [Conf ] Joshua Dunfield , Frank Pfenning Tridirectional typechecking. [Citation Graph (0, 0)][DBLP ] POPL, 2004, pp:281-292 [Conf ] Hongwei Xi , Frank Pfenning Dependent Types in Practical Programming. [Citation Graph (0, 0)][DBLP ] POPL, 1999, pp:214-227 [Conf ] Sungwoo Park , Frank Pfenning , Sebastian Thrun A probabilistic language based upon sampling functions. [Citation Graph (0, 0)][DBLP ] POPL, 2005, pp:171-182 [Conf ] Leaf Petersen , Robert Harper , Karl Crary , Frank Pfenning A type theory for memory allocation and data layout. [Citation Graph (0, 0)][DBLP ] POPL, 2003, pp:172-184 [Conf ] Spiro Michaylov , Frank Pfenning Higher-Order Logic Programming as Constraint Logic Programming. [Citation Graph (0, 0)][DBLP ] PPCP, 1993, pp:210-218 [Conf ] Pablo López , Frank Pfenning , Jeff Polakow , Kevin Watkins Monadic concurrent linear logic programming. [Citation Graph (0, 0)][DBLP ] PPDP, 2005, pp:35-46 [Conf ] Frank Pfenning Logical and Meta-Logical Frameworks (Abstract). [Citation Graph (0, 0)][DBLP ] PPDP, 1999, pp:206- [Conf ] Frank Pfenning Reasoning about Staged Computation. [Citation Graph (0, 0)][DBLP ] SAIG, 2000, pp:5-6 [Conf ] Peter Lee , Frank Pfenning , Gene Rollins , William L. Scherlis The Ergo Support System: An Integrated Set of Tools for Prototyping Integrated Environments. [Citation Graph (0, 0)][DBLP ] Software Development Environments (SDE), 1988, pp:25-34 [Conf ] Robert L. Nord , Frank Pfenning The Ergo Attribute System. [Citation Graph (0, 0)][DBLP ] Software Development Environments (SDE), 1988, pp:110-120 [Conf ] Scott Dietzen , Frank Pfenning A Declarative Alternative to "Assert" in Logic Programming. [Citation Graph (0, 0)][DBLP ] ISLP, 1991, pp:372-386 [Conf ] Michael Kohlhase , Frank Pfenning Unification in a Lambda-Calculus with Intersection Types. [Citation Graph (0, 0)][DBLP ] ILPS, 1993, pp:488-505 [Conf ] Frank Pfenning , Peter Lee LEAP: A Language with Eval And Polymorphism. [Citation Graph (0, 0)][DBLP ] TAPSOFT, Vol.2, 1989, pp:345-359 [Conf ] Joëlle Despeyroux , Frank Pfenning , Carsten Schürmann Primitive Recursion for Higher-Order Abstract Syntax. [Citation Graph (0, 0)][DBLP ] TLCA, 1997, pp:147-163 [Conf ] Jeff Polakow , Frank Pfenning Natural Deduction for Intuitionistic Non-communicative Linear Logic. [Citation Graph (0, 0)][DBLP ] TLCA, 1999, pp:295-309 [Conf ] Penny Anderson , Frank Pfenning Verifying Uniqueness in a Logical Framework. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2004, pp:18-33 [Conf ] 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. [Citation Graph (0, 0)][DBLP ] HUG, 1993, pp:366-370 [Conf ] Carsten Schürmann , Frank Pfenning A Coverage Checking Algorithm for LF. [Citation Graph (0, 0)][DBLP ] TPHOLs, 2003, pp:120-135 [Conf ] Frank Pfenning , Carsten Schürmann Algorithms for Equality and Unification in the Presence of Notational Definitions. [Citation Graph (0, 0)][DBLP ] TYPES, 1998, pp:179-193 [Conf ] Kevin Watkins , Iliano Cervesato , Frank Pfenning , David Walker A Concurrent Logical Framework: The Propositional Fragment. [Citation Graph (0, 0)][DBLP ] TYPES, 2003, pp:355-377 [Conf ] Bernhard Gramlich , Hélène Kirchner , Frank Pfenning Editorial: Strategies in Automated Deduction. [Citation Graph (0, 0)][DBLP ] Ann. Math. Artif. Intell., 2000, v:29, n:1-4, pp:- [Journal ] Alberto Momigliano , Frank Pfenning Higher-Order Pattern Complement and the Strict Lambda-Calculus [Citation Graph (0, 0)][DBLP ] CoRR, 2001, v:0, n:, pp:- [Journal ] Robert Harper , Frank Pfenning On Equivalence and Canonical Forms in the LF Type Theory [Citation Graph (0, 0)][DBLP ] CoRR, 2001, v:0, n:, pp:- [Journal ] Philip Wickline , Peter Lee , Frank Pfenning , Rowan Davies Modal Types as Staging Specifications for Run-Time Code Generation. [Citation Graph (0, 0)][DBLP ] ACM Comput. Surv., 1998, v:30, n:3es, pp:8- [Journal ] Olivier Danvy , Belmina Dzafic , Frank Pfenning On proving syntactic properties of CPS programs. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:26, n:, pp:- [Journal ] Frank Pfenning Preface. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2002, v:70, n:2, pp:- [Journal ] Frank Pfenning Invited talk: Tri-Directional Type Checking. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 2002, v:70, n:1, pp:- [Journal ] Frank Pfenning , Carsten Schürmann Algorithms for Equality and Unification in the Presence of Notational Definitions. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1998, v:17, n:, pp:- [Journal ] Frank Pfenning , Hao-Chi Wong On a modal lambda calculus for S4. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1995, v:1, n:, pp:- [Journal ] J. Polokow , Frank Pfenning Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. [Citation Graph (0, 0)][DBLP ] Electr. Notes Theor. Comput. Sci., 1999, v:20, n:, pp:- [Journal ] Frank Pfenning On the Undecidability of Partial Polymorphic Type Reconstruction. [Citation Graph (0, 0)][DBLP ] Fundam. Inform., 1993, v:19, n:1/2, pp:185-199 [Journal ] Iliano Cervesato , Frank Pfenning A Linear Logical Framework. [Citation Graph (0, 0)][DBLP ] Inf. Comput., 2002, v:179, n:1, pp:19-75 [Journal ] Frank Pfenning Structural Cut Elimination: I. Intuitionistic and Classical Logic. [Citation Graph (0, 0)][DBLP ] Inf. Comput., 2000, v:157, n:1-2, pp:84-141 [Journal ] Rowan Davies , Frank Pfenning A modal analysis of staged computation. [Citation Graph (0, 0)][DBLP ] J. ACM, 2001, v:48, n:3, pp:555-604 [Journal ] Peter B. Andrews , Matthew Bishop , Sunil Issar , Dan Nesmith , Frank Pfenning , Hongwei Xi TPS: A Theorem-Proving System for Classical Type Theory. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 1996, v:16, n:3, pp:321-353 [Journal ] Peter B. Andrews , Chad E. Brown , Frank Pfenning , Matthew Bishop , Sunil Issar , Hongwei Xi ETPS: A System to Help Students Write Formal Proofs. [Citation Graph (0, 0)][DBLP ] J. Autom. Reasoning, 2004, v:32, n:1, pp:75-92 [Journal ] Karl Crary , Aleksey Kliger , Frank Pfenning A monadic analysis of information flow security with mutable state. [Citation Graph (0, 0)][DBLP ] J. Funct. Program., 2005, v:15, n:2, pp:249-291 [Journal ] Aleksandar Nanevski , Frank Pfenning Staged computation with names and necessity. [Citation Graph (0, 0)][DBLP ] J. Funct. Program., 2005, v:15, n:5, pp:893-939 [Journal ] Paliath Narendran , Frank Pfenning , Richard Statman On the Unification Problem for Cartesian Closed Categories. [Citation Graph (0, 0)][DBLP ] J. Symb. Log., 1997, v:62, n:2, pp:636-647 [Journal ] Iliano Cervesato , Frank Pfenning A Linear Spine Calculus. [Citation Graph (0, 0)][DBLP ] J. Log. Comput., 2003, v:13, n:5, pp:639-688 [Journal ] Robert Harper , Frank Pfenning A Module System for a Programming Language Based on the LF Logical Framework. [Citation Graph (0, 0)][DBLP ] J. Log. Comput., 1998, v:8, n:1, pp:5-31 [Journal ] Scott Dietzen , Frank Pfenning Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization. [Citation Graph (0, 0)][DBLP ] Machine Learning, 1992, v:9, n:, pp:23-55 [Journal ] Frank Pfenning , Rowan Davies A judgmental reconstruction of modal logic. [Citation Graph (0, 0)][DBLP ] Mathematical Structures in Computer Science, 2001, v:11, n:4, pp:511-540 [Journal ] Wilfried Sieg , Frank Pfenning Note by the Guest Editors. [Citation Graph (0, 0)][DBLP ] Studia Logica, 1998, v:60, n:1, pp:1- [Journal ] Iliano Cervesato , Joshua S. Hodas , Frank Pfenning Efficient resource management for linear logic proof search. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2000, v:232, n:1-2, pp:133-163 [Journal ] Christopher Colby , Karl Crary , Robert Harper , Peter Lee , Frank Pfenning Automated techniques for provably safe mobile code. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2003, v:290, n:2, pp:1175-1199 [Journal ] Frank Pfenning , Peter Lee Metacircularity in the Polymorphic lambda-Calculus. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 1991, v:89, n:1, pp:137-159 [Journal ] Carsten Schürmann , Joëlle Despeyroux , Frank Pfenning Primitive recursion for higher-order abstract syntax. [Citation Graph (0, 0)][DBLP ] Theor. Comput. Sci., 2001, v:266, n:1-2, pp:1-57 [Journal ] Martín Abadi , Leonid Libkin , Frank Pfenning Editorial. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2002, v:3, n:3, pp:335-335 [Journal ] Alberto Momigliano , Frank Pfenning Higher-order pattern complement and the strict lambda-calculus. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2003, v:4, n:4, pp:493-529 [Journal ] Robert Harper , Frank Pfenning On equivalence and canonical forms in the LF type theory. [Citation Graph (0, 0)][DBLP ] ACM Trans. Comput. Log., 2005, v:6, n:1, pp:61-101 [Journal ] Frank Pfenning Subtyping and intersection types revisited. [Citation Graph (0, 0)][DBLP ] ICFP, 2007, pp:219- [Conf ] Uluc Saranli , Frank Pfenning Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. [Citation Graph (0, 0)][DBLP ] ICRA, 2007, pp:3705-3710 [Conf ] Frank Pfenning On a Logical Foundation for Explicit Substitutions. [Citation Graph (0, 0)][DBLP ] RTA, 2007, pp:19- [Conf ] Frank Pfenning On a Logical Foundation for Explicit Substitutions. [Citation Graph (0, 0)][DBLP ] TLCA, 2007, pp:1- [Conf ] Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. [Citation Graph (, )][DBLP ] Session Types as Intuitionistic Linear Propositions. [Citation Graph (, )][DBLP ] An Authorization Logic With Explicit Time. [Citation Graph (, )][DBLP ] Linear Logical Algorithms. [Citation Graph (, )][DBLP ] Towards a type theory of contexts. [Citation Graph (, )][DBLP ] Substructural Operational Semantics as Ordered Logic Programming. [Citation Graph (, )][DBLP ] Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. [Citation Graph (, )][DBLP ] Consumable Credentials in Linear-Logic-Based Access-Control Systems. [Citation Graph (, )][DBLP ] Linear logical approximations. [Citation Graph (, )][DBLP ] A Proof-Carrying File System. [Citation Graph (, )][DBLP ] Refinement Types as Proof Irrelevance. [Citation Graph (, )][DBLP ] A Bidirectional Refinement Type System for LF. [Citation Graph (, )][DBLP ] Specifying Properties of Concurrent Computations in CLF. [Citation Graph (, )][DBLP ] Intuitionistic Letcc via Labelled Deduction. [Citation Graph (, )][DBLP ] Search in 0.012secs, Finished in 0.020secs