 | 2009 |
|---|
| 130 |       | Sean McLaughlin,
Frank Pfenning:
Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method.
CADE 2009: 230-244 |
| 129 | | Frank Pfenning,
Robert J. Simmons:
Substructural Operational Semantics as Ordered Logic Programming.
LICS 2009: 101-110 |
| 128 | | Robert J. Simmons,
Frank Pfenning:
Linear logical approximations.
PEPM 2009: 9-20 |
| 127 | | William Lovas,
Frank Pfenning:
Refinement Types as Proof Irrelevance.
TLCA 2009: 157-171 |
| 126 | | Jason Reed,
Frank Pfenning:
Intuitionistic Letcc via Labelled Deduction.
Electr. Notes Theor. Comput. Sci. 231: 91-111 (2009) |
| 2008 |
|---|
| 125 | | Henry DeYoung,
Deepak Garg,
Frank Pfenning:
An Authorization Logic With Explicit Time.
CSF 2008: 133-145 |
| 124 | | Robert J. Simmons,
Frank Pfenning:
Linear Logical Algorithms.
ICALP (2) 2008: 336-347 |
| 123 | | Sean McLaughlin,
Frank Pfenning:
Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic.
LPAR 2008: 174-181 |
| 122 | | Aleksandar Nanevski,
Frank Pfenning,
Brigitte Pientka:
Contextual modal type theory.
ACM Trans. Comput. Log. 9(3): (2008) |
| 121 | | Sungwoo Park,
Frank Pfenning,
Sebastian Thrun:
A probabilistic language based on sampling functions.
ACM Trans. Program. Lang. Syst. 31(1): (2008) |
| 120 | | William Lovas,
Frank Pfenning:
A Bidirectional Refinement Type System for LF.
Electr. Notes Theor. Comput. Sci. 196: 113-128 (2008) |
| 119 | | Kevin Watkins,
Iliano Cervesato,
Frank Pfenning,
David Walker:
Specifying Properties of Concurrent Computations in CLF.
Electr. Notes Theor. Comput. Sci. 199: 67-87 (2008) |
| 118 | | Kaustuv Chaudhuri,
Frank Pfenning,
Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method.
J. Autom. Reasoning 40(2-3): 133-177 (2008) |
| 2007 |
|---|
| 117 |  | Frank Pfenning:
Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, Proceedings
Springer 2007 |
| 116 | | Frank Pfenning:
Subtyping and intersection types revisited.
ICFP 2007: 219 |
| 115 | | Uluc Saranli,
Frank Pfenning:
Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems.
ICRA 2007: 3705-3710 |
| 114 | | Kevin D. Bowers,
Lujo Bauer,
Deepak Garg,
Frank Pfenning,
Michael K. Reiter:
Consumable Credentials in Linear-Logic-Based Access-Control Systems.
NDSS 2007 |
| 113 | | Frank Pfenning:
On a Logical Foundation for Explicit Substitutions.
RTA 2007: 19 |
| 112 | | Frank Pfenning:
On a Logical Foundation for Explicit Substitutions.
TLCA 2007: 1 |
| 2006 |
|---|
| 111 | | Frank Pfenning:
Term Rewriting and Applications, 17th International Conference, RTA 2006, Seattle, WA, USA, August 12-14, 2006, Proceedings
Springer 2006 |
| 110 | | Deepak Garg,
Frank Pfenning:
Non-Interference in Constructive Authorization Logic.
CSFW 2006: 283-296 |
| 109 | | Deepak Garg,
Lujo Bauer,
Kevin D. Bowers,
Frank Pfenning,
Michael K. Reiter:
A Linear Logic of Authorization and Knowledge.
ESORICS 2006: 297-312 |
| 108 | | Kaustuv Chaudhuri,
Frank Pfenning,
Greg Price:
A Logical Characterization of Forward and Backward Chaining in the Inverse Method.
IJCAR 2006: 97-111 |
| 2005 |
|---|
| 107 | | Kaustuv Chaudhuri,
Frank Pfenning:
A Focusing Inverse Method Theorem Prover for First-Order Linear Logic.
CADE 2005: 69-83 |
| 106 | | Deepak Garg,
Frank Pfenning:
Type-Directed Concurrency.
CONCUR 2005: 6-20 |
| 105 | | Kaustuv Chaudhuri,
Frank Pfenning:
Focusing the Inverse Method for Linear Logic.
CSL 2005: 200-215 |
| 104 | | Frank Pfenning:
Towards a type theory of contexts.
MERLIN 2005: 1 |
| 103 | | Sungwoo Park,
Frank Pfenning,
Sebastian Thrun:
A probabilistic language based upon sampling functions.
POPL 2005: 171-182 |
| 102 | | Pablo López,
Frank Pfenning,
Jeff Polakow,
Kevin Watkins:
Monadic concurrent linear logic programming.
PPDP 2005: 35-46 |
| 101 | | Robert Harper,
Frank Pfenning:
On equivalence and canonical forms in the LF type theory.
ACM Trans. Comput. Log. 6(1): 61-101 (2005) |
| 100 | | Karl Crary,
Aleksey Kliger,
Frank Pfenning:
A monadic analysis of information flow security with mutable state.
J. Funct. Program. 15(2): 249-291 (2005) |
| 99 | | Aleksandar Nanevski,
Frank Pfenning:
Staged computation with names and necessity.
J. Funct. Program. 15(5): 893-939 (2005) |
| 2004 |
|---|
| 98 | | Frank Pfenning:
Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk).
APLAS 2004: 196 |
| 97 | | Tom Murphy VII,
Karl Crary,
Robert Harper,
Frank Pfenning:
A Symmetric Modal Lambda Calculus for Distributed Computing.
LICS 2004: 286-295 |
| 96 | | Joshua Dunfield,
Frank Pfenning:
Tridirectional typechecking.
POPL 2004: 281-292 |
| 95 | | Penny Anderson,
Frank Pfenning:
Verifying Uniqueness in a Logical Framework.
TPHOLs 2004: 18-33 |
| 94 | | 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. Reasoning 32(1): 75-92 (2004) |
| 2003 |
|---|
| 93 | | Frank Pfenning,
Yannis Smaragdakis:
Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, Proceedings
Springer 2003 |
| 92 | | Brigitte Pientka,
Frank Pfenning:
Optimizing Higher-Order Pattern Unification.
CADE 2003: 473-487 |
| 91 | | Joshua Dunfield,
Frank Pfenning:
Type Assignment for Intersections and Unions in Call-by-Value Languages.
FoSSaCS 2003: 250-266 |
| 90 | | 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 |
| 89 | | Aleksandar Nanevski,
Brigitte Pientka,
Frank Pfenning:
A modal foundation for meta-variables.
MERLIN 2003 |
| 88 | | Leaf Petersen,
Robert Harper,
Karl Crary,
Frank Pfenning:
A type theory for memory allocation and data layout.
POPL 2003: 172-184 |
| 87 | | Carsten Schürmann,
Frank Pfenning:
A Coverage Checking Algorithm for LF.
TPHOLs 2003: 120-135 |
| 86 | | Kevin Watkins,
Iliano Cervesato,
Frank Pfenning,
David Walker:
A Concurrent Logical Framework: The Propositional Fragment.
TYPES 2003: 355-377 |
| 85 | | Alberto Momigliano,
Frank Pfenning:
Higher-order pattern complement and the strict lambda-calculus.
ACM Trans. Comput. Log. 4(4): 493-529 (2003) |
| 84 | | Iliano Cervesato,
Frank Pfenning:
A Linear Spine Calculus.
J. Log. Comput. 13(5): 639-688 (2003) |
| 83 | | 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) |
| 2002 |
|---|
| 82 | | 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 |
| 81 | | Martín Abadi,
Leonid Libkin,
Frank Pfenning:
Editorial.
ACM Trans. Comput. Log. 3(3): 335-335 (2002) |
| 80 | | Frank Pfenning:
Invited talk: Tri-Directional Type Checking.
Electr. Notes Theor. Comput. Sci. 70(1): (2002) |
| 79 | | Frank Pfenning:
Preface.
Electr. Notes Theor. Comput. Sci. 70(2): (2002) |
| 78 | | Iliano Cervesato,
Frank Pfenning:
A Linear Logical Framework.
Inf. Comput. 179(1): 19-75 (2002) |
| 2001 |
|---|
| 77 | | Frank Pfenning:
Intensionality, Extensionality, and Proof Irrelevance in Modal Type Theory.
LICS 2001 |
| 76 | | Frank Pfenning:
Logical Frameworks.
Handbook of Automated Reasoning 2001: 1063-1147 |
| 75 | | Alberto Momigliano,
Frank Pfenning:
Higher-Order Pattern Complement and the Strict Lambda-Calculus
CoRR cs.LO/0109072: (2001) |
| 74 | | Robert Harper,
Frank Pfenning:
On Equivalence and Canonical Forms in the LF Type Theory
CoRR cs.LO/0110028: (2001) |
| 73 | | Rowan Davies,
Frank Pfenning:
A modal analysis of staged computation.
J. ACM 48(3): 555-604 (2001) |
| 72 | | Frank Pfenning,
Rowan Davies:
A judgmental reconstruction of modal logic.
Mathematical Structures in Computer Science 11(4): 511-540 (2001) |
| 71 | | 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 |
|---|
| 70 | | Rowan Davies,
Frank Pfenning:
Intersection types and computational effects.
ICFP 2000: 198-208 |
| 69 | | Frank Pfenning:
On the Logical Foundations of Staged Computation (Abstract of Invited Talk).
PEPM 2000: 33 |
| 68 | | Frank Pfenning:
Reasoning about Staged Computation.
SAIG 2000: 5-6 |
| 67 | | Bernhard Gramlich,
Hélène Kirchner,
Frank Pfenning:
Editorial: Strategies in Automated Deduction.
Ann. Math. Artif. Intell. 29(1-4): (2000) |
| 66 | | Frank Pfenning:
Structural Cut Elimination: I. Intuitionistic and Classical Logic.
Inf. Comput. 157(1-2): 84-141 (2000) |
| 65 | | Iliano Cervesato,
Joshua S. Hodas,
Frank Pfenning:
Efficient resource management for linear logic proof search.
Theor. Comput. Sci. 232(1-2): 133-163 (2000) |
| 1999 |
|---|
| 64 | | Alberto Momigliano,
Frank Pfenning:
The Relative Complement Problem for Higher-Order Patterns.
APPIA-GULP-PRODE 1999: 497-512 |
| 63 | | Frank Pfenning,
Carsten Schürmann:
System Description: Twelf - A Meta-Logical Framework for Deductive Systems.
CADE 1999: 202-206 |
| 62 | | Alberto Momigliano,
Frank Pfenning:
The Relative Complement Problem for Higher-Order Patterns.
ICLP 1999: 380-394 |
| 61 | | Hongwei Xi,
Frank Pfenning:
Dependent Types in Practical Programming.
POPL 1999: 214-227 |
| 60 | | Frank Pfenning:
Logical and Meta-Logical Frameworks (Abstract).
PPDP 1999: 206 |
| 59 | | Jeff Polakow,
Frank Pfenning:
Natural Deduction for Intuitionistic Non-communicative Linear Logic.
TLCA 1999: 295-309 |
| 58 | | J. Polokow,
Frank Pfenning:
Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic.
Electr. Notes Theor. Comput. Sci. 20: (1999) |
| 57 | | Olivier Danvy,
Belmina Dzafic,
Frank Pfenning:
On proving syntactic properties of CPS programs.
Electr. Notes Theor. Comput. Sci. 26: (1999) |
| 1998 |
|---|
| 56 | | Frank Pfenning:
Reasoning About Deductions in Linear Logic (Abstract of Invited Talk).
CADE 1998: 1-2 |
| 55 | | Carsten Schürmann,
Frank Pfenning:
Automated Theorem Proving in a Simple Meta-Logic for LF.
CADE 1998: 286-300 |
| 54 | | Philip Wickline,
Peter Lee,
Frank Pfenning:
Run-time Code Generation and Modal-ML.
PLDI 1998: 224-235 |
| 53 | | Hongwei Xi,
Frank Pfenning:
Eliminating Array Bound Checking Through Dependent Types.
PLDI 1998: 249-257 |
| 52 | | Frank Pfenning,
Carsten Schürmann:
Algorithms for Equality and Unification in the Presence of Notational Definitions.
TYPES 1998: 179-193 |
| 51 | | 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) |
| 50 | | Frank Pfenning,
Carsten Schürmann:
Algorithms for Equality and Unification in the Presence of Notational Definitions.
Electr. Notes Theor. Comput. Sci. 17: (1998) |
| 49 | | 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) |
| 48 | | Wilfried Sieg,
Frank Pfenning:
Note by the Guest Editors.
Studia Logica 60(1): 1 (1998) |
| 1997 |
|---|
| 47 | | Iliano Cervesato,
Frank Pfenning:
Linear Higher-Order Pre-Unification.
LICS 1997: 422-433 |
| 46 | | Joëlle Despeyroux,
Frank Pfenning,
Carsten Schürmann:
Primitive Recursion for Higher-Order Abstract Syntax.
TLCA 1997: 147-163 |
| 45 | | Paliath Narendran,
Frank Pfenning,
Richard Statman:
On the Unification Problem for Cartesian Closed Categories.
J. Symb. Log. 62(2): 636-647 (1997) |
| 1996 |
|---|
| 44 | | Frank Pfenning:
The Practice of Logical Frameworks.
CAAP 1996: 119-134 |
| 43 | | Iliano Cervesato,
Joshua S. Hodas,
Frank Pfenning:
Efficient Resource Management for Linear Logic Proof Search.
ELP 1996: 67-81 |
| 42 | | Ekkehard Rohwedder,
Frank Pfenning:
Mode and Termination Checking for Higher-Order Logic Programs.
ESOP 1996: 296-310 |
| 41 | | Gilles Dowek,
Thérèse Hardin,
Claude Kirchner,
Frank Pfenning:
Unification via Explicit Substitutions: The Case of Higher-Order Patterns.
JICSLP 1996: 259-273 |
| 40 | | Iliano Cervesato,
Frank Pfenning:
A Linear Logical Framework.
LICS 1996: 264-275 |
| 39 | | Rowan Davies,
Frank Pfenning:
A Modal Analysis of Staged Computation.
POPL 1996: 258-270 |
| 38 | | Peter B. Andrews,
Matthew Bishop,
Sunil Issar,
Dan Nesmith,
Frank Pfenning,
Hongwei Xi:
TPS: A Theorem-Proving System for Classical Type Theory.
J. Autom. Reasoning 16(3): 321-353 (1996) |
| 1995 |
|---|
| 37 | | Frank Pfenning:
Structural Cut Elimination
LICS 1995: 156-166 |
| 36 | | Frank Pfenning,
Hao-Chi Wong:
On a modal lambda calculus for S4.
Electr. Notes Theor. Comput. Sci. 1: (1995) |
| 1994 |
|---|
| 35 | | Frank Pfenning:
Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 16-22, 1994, Proceedings
Springer 1994 |
| 34 | | Frank Pfenning:
Elf: A Meta-Language for Deductive Systems (System Descrition).
CADE 1994: 811-815 |
| 1993 |
|---|
| 33 | | 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 |
| 32 | | Michael Kohlhase,
Frank Pfenning:
Unification in a Lambda-Calculus with Intersection Types.
ILPS 1993: 488-505 |
| 31 | | Paliath Narendran,
Frank Pfenning,
Richard Statman:
On the Unification Problem for Cartesian Closed Categories
LICS 1993: 57-63 |
| 30 | | Spiro Michaylov,
Frank Pfenning:
Higher-Order Logic Programming as Constraint Logic Programming.
PPCP 1993: 210-218 |
| 29 | | Frank Pfenning:
On the Undecidability of Partial Polymorphic Type Reconstruction.
Fundam. Inform. 19(1/2): 185-199 (1993) |
| 1992 |
|---|
| 28 | | Frank Pfenning,
Ekkehard Rohwedder:
Implementing the Meta-Theory of Deductive Systems.
CADE 1992: 537-551 |
| 27 | | John Hannan,
Frank Pfenning:
Compiler Verification in LF
LICS 1992: 407-418 |
| 26 | | Gopalan Nadathur,
Frank Pfenning:
The Type System of a Higher-Order Logic Programming Language.
Types in Logic Programming 1992: 245-283 |
| 25 | | Frank Pfenning:
Dependent Types in Logic Programming.
Types in Logic Programming 1992: 285-311 |
| 24 | | Scott Dietzen,
Frank Pfenning:
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization.
Machine Learning 9: 23-55 (1992) |
| 1991 |
|---|
| 23 | | Spiro Michaylov,
Frank Pfenning:
Natural Semantics and Some of Its Meta-Theory in Elf.
ELP 1991: 299-344 |
| 22 | | Scott Dietzen,
Frank Pfenning:
A Declarative Alternative to "Assert" in Logic Programming.
ISLP 1991: 372-386 |
| 21 | | Frank Pfenning:
Unification and Anti-Unification in the Calculus of Constructions
LICS 1991: 74-85 |
| 20 | | Spiro Michaylov,
Frank Pfenning:
Compiling the Polymorphic Lambda-Calculus.
PEPM 1991: 285-296 |
| 19 | | Tim Freeman,
Frank Pfenning:
Refinement Types for ML.
PLDI 1991: 268-277 |
| 18 | | Dale Miller,
Gopalan Nadathur,
Frank Pfenning,
Andre Scedrov:
Uniform Proofs as a Foundation for Logic Programming.
Ann. Pure Appl. Logic 51(1-2): 125-157 (1991) |
| 17 | | Frank Pfenning,
Peter Lee:
Metacircularity in the Polymorphic lambda-Calculus.
Theor. Comput. Sci. 89(1): 137-159 (1991) |
| 1990 |
|---|
| 16 | | Frank Pfenning,
Dan Nesmith:
Presenting Intuitive Deductions via Symmetric Simplification.
CADE 1990: 336-350 |
| 15 | | Peter B. Andrews,
Sunil Issar,
Dan Nesmith,
Frank Pfenning:
The TPS Theorem Proving System.
CADE 1990: 641-642 |
| 14 | | Amy P. Felty,
Elsa L. Gunter,
Dale Miller,
Frank Pfenning:
Tutorial on Lambda-Prolog.
CADE 1990: 682 |
| 13 | | Frank Pfenning:
Types in Logic Programming.
ICLP 1990: 786 |
| 1989 |
|---|
| 12 | | Frank Pfenning:
Elf: A Language for Logic Definition and Verified Metaprogramming
LICS 1989: 313-322 |
| 11 | | Scott Dietzen,
Frank Pfenning:
Higher-Order and Modal Logic as a Framework for Explanation-Based Generalization.
ML 1989: 447-449 |
| 10 | | Frank Pfenning,
Christine Paulin-Mohring:
Inductively Defined Types in the Calculus of Constructions.
Mathematical Foundations of Programming Semantics 1989: 209-228 |
| 9 | | Frank Pfenning,
Peter Lee:
LEAP: A Language with Eval And Polymorphism.
TAPSOFT, Vol.2 1989: 345-359 |
| 1988 |
|---|
| 8 | | Frank Pfenning:
Single Axioms in the Implicational Propositional Calculus.
CADE 1988: 710-713 |
| 7 | | Peter B. Andrews,
Sunil Issar,
Daniel Nesmith,
Frank Pfenning:
The TPS Theorem Proving System.
CADE 1988: 760-761 |
| 6 | | Frank Pfenning:
Partial Polymorphic Type Inference and Higher-Order Unification.
LISP and Functional Programming 1988: 153-163 |
| 5 | | Frank Pfenning,
Conal Elliott:
Higher-Order Abstract Syntax.
PLDI 1988: 199-208 |
| 4 | | Robert L. Nord,
Frank Pfenning:
The Ergo Attribute System.
Software Development Environments (SDE) 1988: 110-120 |
| 3 | | 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 |
| 1986 |
|---|
| 2 | | Peter B. Andrews,
Frank Pfenning,
Sunil Issar,
C. P. Klapper:
The TPS Theorem Proving System.
CADE 1986: 663-664 |
| 1984 |
|---|
| 1 | | Frank Pfenning:
Analytic and Non-analytic Proofs.
CADE 1984: 394-413 |
