dblp.uni-trier.dewww.uni-trier.de

Frank Pfenning Vis

List of publications from the DBLP Bibliography Server - FAQ
Coauthor Index - Ask others: ACM DL/Guide - CiteSeerX - CSB - MetaPress - Google - Bing - Yahoo
Home Page

*2009
129EESean McLaughlin, Frank Pfenning: Efficient Intuitionistic Theorem Proving with the Polarized Inverse Method. CADE 2009: 230-244
128EERobert J. Simmons, Frank Pfenning: Linear logical approximations. PEPM 2009: 9-20
127EEWilliam Lovas, Frank Pfenning: Refinement Types as Proof Irrelevance. TLCA 2009: 157-171
126EEJason Reed, Frank Pfenning: Intuitionistic Letcc via Labelled Deduction. Electr. Notes Theor. Comput. Sci. 231: 91-111 (2009)
2008
125EEHenry DeYoung, Deepak Garg, Frank Pfenning: An Authorization Logic With Explicit Time. CSF 2008: 133-145
124EERobert J. Simmons, Frank Pfenning: Linear Logical Algorithms. ICALP (2) 2008: 336-347
123EESean McLaughlin, Frank Pfenning: Imogen: Focusing the Polarized Inverse Method for Intuitionistic Propositional Logic. LPAR 2008: 174-181
122EEAleksandar Nanevski, Frank Pfenning, Brigitte Pientka: Contextual modal type theory. ACM Trans. Comput. Log. 9(3): (2008)
121EESungwoo Park, Frank Pfenning, Sebastian Thrun: A probabilistic language based on sampling functions. ACM Trans. Program. Lang. Syst. 31(1): (2008)
120EEWilliam Lovas, Frank Pfenning: A Bidirectional Refinement Type System for LF. Electr. Notes Theor. Comput. Sci. 196: 113-128 (2008)
119EEKevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker: Specifying Properties of Concurrent Computations in CLF. Electr. Notes Theor. Comput. Sci. 199: 67-87 (2008)
118EEKaustuv 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
116EEFrank Pfenning: Subtyping and intersection types revisited. ICFP 2007: 219
115EEUluc Saranli, Frank Pfenning: Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning Problems. ICRA 2007: 3705-3710
114EEKevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter: Consumable Credentials in Linear-Logic-Based Access-Control Systems. NDSS 2007
113EEFrank Pfenning: On a Logical Foundation for Explicit Substitutions. RTA 2007: 19
112EEFrank 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
110EEDeepak Garg, Frank Pfenning: Non-Interference in Constructive Authorization Logic. CSFW 2006: 283-296
109EEDeepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter: A Linear Logic of Authorization and Knowledge. ESORICS 2006: 297-312
108EEKaustuv Chaudhuri, Frank Pfenning, Greg Price: A Logical Characterization of Forward and Backward Chaining in the Inverse Method. IJCAR 2006: 97-111
2005
107EEKaustuv Chaudhuri, Frank Pfenning: A Focusing Inverse Method Theorem Prover for First-Order Linear Logic. CADE 2005: 69-83
106EEDeepak Garg, Frank Pfenning: Type-Directed Concurrency. CONCUR 2005: 6-20
105EEKaustuv Chaudhuri, Frank Pfenning: Focusing the Inverse Method for Linear Logic. CSL 2005: 200-215
104EEFrank Pfenning: Towards a type theory of contexts. MERLIN 2005: 1
103EESungwoo Park, Frank Pfenning, Sebastian Thrun: A probabilistic language based upon sampling functions. POPL 2005: 171-182
102EEPablo López, Frank Pfenning, Jeff Polakow, Kevin Watkins: Monadic concurrent linear logic programming. PPDP 2005: 35-46
101EERobert Harper, Frank Pfenning: On equivalence and canonical forms in the LF type theory. ACM Trans. Comput. Log. 6(1): 61-101 (2005)
100EEKarl Crary, Aleksey Kliger, Frank Pfenning: A monadic analysis of information flow security with mutable state. J. Funct. Program. 15(2): 249-291 (2005)
99EEAleksandar Nanevski, Frank Pfenning: Staged computation with names and necessity. J. Funct. Program. 15(5): 893-939 (2005)
2004
98EEFrank Pfenning: Substructural Operational Semantics and Linear Destination-Passing Style (Invited Talk). APLAS 2004: 196
97EETom Murphy VII, Karl Crary, Robert Harper, Frank Pfenning: A Symmetric Modal Lambda Calculus for Distributed Computing. LICS 2004: 286-295
96EEJoshua Dunfield, Frank Pfenning: Tridirectional typechecking. POPL 2004: 281-292
95EEPenny Anderson, Frank Pfenning: Verifying Uniqueness in a Logical Framework. TPHOLs 2004: 18-33
94EEPeter 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
92EEBrigitte Pientka, Frank Pfenning: Optimizing Higher-Order Pattern Unification. CADE 2003: 473-487
91EEJoshua 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
89EEAleksandar Nanevski, Brigitte Pientka, Frank Pfenning: A modal foundation for meta-variables. MERLIN 2003
88EELeaf Petersen, Robert Harper, Karl Crary, Frank Pfenning: A type theory for memory allocation and data layout. POPL 2003: 172-184
87EECarsten Schürmann, Frank Pfenning: A Coverage Checking Algorithm for LF. TPHOLs 2003: 120-135
86EEKevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker: A Concurrent Logical Framework: The Propositional Fragment. TYPES 2003: 355-377
85EEAlberto Momigliano, Frank Pfenning: Higher-order pattern complement and the strict lambda-calculus. ACM Trans. Comput. Log. 4(4): 493-529 (2003)
84EEIliano 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
82EEBor-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
81EEMartín Abadi, Leonid Libkin, Frank Pfenning: Editorial. ACM Trans. Comput. Log. 3(3): 335-335 (2002)
80EEFrank Pfenning: Invited talk: Tri-Directional Type Checking. Electr. Notes Theor. Comput. Sci. 70(1): (2002)
79EEFrank Pfenning: Preface. Electr. Notes Theor. Comput. Sci. 70(2): (2002)
78EEIliano 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
75EEAlberto Momigliano, Frank Pfenning: Higher-Order Pattern Complement and the Strict Lambda-Calculus CoRR cs.LO/0109072: (2001)
74EERobert Harper, Frank Pfenning: On Equivalence and Canonical Forms in the LF Type Theory CoRR cs.LO/0110028: (2001)
73EERowan 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)
71EECarsten Schürmann, Joëlle Despeyroux, Frank Pfenning: Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1-2): 1-57 (2001)
2000
70EERowan Davies, Frank Pfenning: Intersection types and computational effects. ICFP 2000: 198-208
69EEFrank Pfenning: On the Logical Foundations of Staged Computation (Abstract of Invited Talk). PEPM 2000: 33
68EEFrank 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)
65EEIliano 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
63EEFrank 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
61EEHongwei Xi, Frank Pfenning: Dependent Types in Practical Programming. POPL 1999: 214-227
60 Frank Pfenning: Logical and Meta-Logical Frameworks (Abstract). PPDP 1999: 206
59EEJeff Polakow, Frank Pfenning: Natural Deduction for Intuitionistic Non-communicative Linear Logic. TLCA 1999: 295-309
58EEJ. Polokow, Frank Pfenning: Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear Logic. Electr. Notes Theor. Comput. Sci. 20: (1999)
57EEOlivier Danvy, Belmina Dzafic, Frank Pfenning: On proving syntactic properties of CPS programs. Electr. Notes Theor. Comput. Sci. 26: (1999)
1998
56EEFrank Pfenning: Reasoning About Deductions in Linear Logic (Abstract of Invited Talk). CADE 1998: 1-2
55EECarsten 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
52EEFrank Pfenning, Carsten Schürmann: Algorithms for Equality and Unification in the Presence of Notational Definitions. TYPES 1998: 179-193
51EEPhilip Wickline, Peter Lee, Frank Pfenning, Rowan Davies: Modal Types as Staging Specifications for Run-Time Code Generation. ACM Comput. Surv. 30(3es): 8 (1998)
50EEFrank 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
47EEIliano 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
44EEFrank Pfenning: The Practice of Logical Frameworks. CAAP 1996: 119-134
43EEIliano Cervesato, Joshua S. Hodas, Frank Pfenning: Efficient Resource Management for Linear Logic Proof Search. ELP 1996: 67-81
42EEEkkehard 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
39EERowan 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
36EEFrank 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
34EEFrank Pfenning: Elf: A Meta-Language for Deductive Systems (System Descrition). CADE 1994: 811-815
1993
33EEPeter 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
28EEFrank 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
23EESpiro 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
16EEFrank Pfenning, Dan Nesmith: Presenting Intuitive Deductions via Symmetric Simplification. CADE 1990: 336-350
15EEPeter B. Andrews, Sunil Issar, Dan Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1990: 641-642
14EEAmy 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
10EEFrank Pfenning, Christine Paulin-Mohring: Inductively Defined Types in the Calculus of Constructions. Mathematical Foundations of Programming Semantics 1989: 209-228
9EEFrank Pfenning, Peter Lee: LEAP: A Language with Eval And Polymorphism. TAPSOFT, Vol.2 1989: 345-359
1988
8EEFrank Pfenning: Single Axioms in the Implicational Propositional Calculus. CADE 1988: 710-713
7EEPeter B. Andrews, Sunil Issar, Daniel Nesmith, Frank Pfenning: The TPS Theorem Proving System. CADE 1988: 760-761
6EEFrank 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
2EEPeter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper: The TPS Theorem Proving System. CADE 1986: 663-664
1984
1EEFrank Pfenning: Analytic and Non-analytic Proofs. CADE 1984: 394-413

Coauthor Index

1Martín Abadi [81]
2Penny Anderson [95]
3Peter B. Andrews [2] [7] [15] [33] [38] [94]
4Lujo Bauer [109] [114]
5Matthew Bishop [33] [38] [94]
6Kevin D. Bowers [109] [114]
7Chad E. Brown [94]
8Iliano Cervesato [40] [43] [47] [65] [78] [84] [86] [119]
9Bor-Yuh Evan Chang [82]
10Kaustuv Chaudhuri [105] [107] [108] [118]
11Christopher Colby [83]
12Karl Crary [82] [83] [88] [97] [100]
13Olivier Danvy [57]
14Rowan Davies [39] [51] [70] [72] [73]
15Margaret DeLap [82]
16Henry DeYoung [125]
17Joëlle Despeyroux [46] [71]
18Scott Dietzen [11] [22] [24]
19Gilles Dowek [41]
20Joshua Dunfield [91] [96]
21Belmina Dzafic [57]
22Conal Elliott (Conal M. Elliott) [5]
23Amy P. Felty [14]
24Tim Freeman [19]
25Deepak Garg [106] [109] [110] [114] [125]
26Geoffrey J. Gordon [90]
27Bernhard Gramlich [67]
28Elsa L. Gunter [14]
29John Hannan [27]
30Thérèse Hardin [41]
31Robert Harper [49] [74] [82] [83] [88] [97] [101]
32Joshua S. Hodas [43] [65]
33Sunil Issar [2] [7] [15] [33] [38] [94]
34Claude Kirchner [41]
35Hélène Kirchner [67]
36C. P. Klapper [2]
37Aleksey Kliger [100]
38Mary Koes (Mary Berna-Koes, Mary Berna) [90]
39Michael Kohlhase [32]
40Peter Lee [3] [9] [17] [51] [54] [83]
41Leonid Libkin [81]
42Brad Lisien [90]
43Jason Liszka [82]
44Pablo López [102]
45William Lovas [120] [127]
46Sean McLaughlin [123] [129]
47Spiro Michaylov [20] [23] [30]
48Dale Miller [14] [18]
49Alberto Momigliano [62] [64] [75] [85]
50Gopalan Nadathur [18] [26]
51Aleksandar Nanevski [89] [99] [122]
52Paliath Narendran [31] [45]
53Daniel Nesmith (Dan Nesmith) [7] [15] [16] [33] [38]
54Robert L. Nord [4]
55Sungwoo Park [103] [121]
56Christine Paulin-Mohring [10]
57Leaf Petersen [88]
58Brigitte Pientka [89] [92] [122]
59Jeff Polakow (Jeffrey Polakow) [59] [102]
60J. Polokow [58]
61Greg Price [108] [118]
62Jason Reed [126]
63Michael K. Reiter [109] [114]
64Ekkehard Rohwedder [28] [42]
65Gene Rollins [3]
66Uluc Saranli [115]
67Andre Scedrov [18]
68William L. Scherlis (Bill Scherlis) [3]
69Carsten Schürmann [46] [50] [52] [55] [63] [71] [87]
70Brennan Sellner [90]
71Wilfried Sieg [48]
72Robert J. Simmons [124] [128]
73Yannis Smaragdakis [93]
74Richard Statman [31] [45]
75Sebastian Thrun [90] [103] [121]
76Tom Murphy VII [82] [97]
77David Walker [86] [119]
78Kevin Watkins [86] [102] [119]
79Philip Wickline [51] [54]
80Hao-Chi Wong [36]
81Hongwei Xi [33] [38] [53] [61] [94]

Colors in the list of coauthors

Copyright © Tue Nov 3 08:52:44 2009 by Michael Ley (ley@uni-trier.de)