Frank Pfenning - researchr profile publications

researchr

You are not signed in
Sign in
Sign up

2009

Intuitionistic Letcc via Labelled DeductionJason Reed, Frank Pfenning. ENTCS, 231:91-111, 2009. [doi]

Linear logical approximationsRobert J. Simmons, Frank Pfenning. PEPM 2009: 9-20 [doi]

2008

2007

Consumable Credentials in Linear-Logic-Based Access-Control SystemsKevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, Michael K. Reiter. ndss 2007: [doi]

Automated Deduction - CADE-21, 21st International Conference on Automated Deduction, Bremen, Germany, July 17-20, 2007, ProceedingsFrank Pfenning, editor, Volume 4603 of Lecture Notes in Computer Science, Springer, 2007.

On a Logical Foundation for Explicit SubstitutionsFrank Pfenning. RTA 2007: 19 [doi]

Using Constrained Intuitionistic Linear Logic for Hybrid Robotic Planning ProblemsUluc Saranli, Frank Pfenning. icra 2007: 3705-3710 [doi]

2006

A Linear Logic of Authorization and KnowledgeDeepak Garg, Lujo Bauer, Kevin D. Bowers, Frank Pfenning, Michael K. Reiter. esorics 2006: 297-312 [doi]

2005

2004

2003

Automated techniques for provably safe mobile codeChristopher Colby, Karl Crary, Robert Harper, Peter Lee, Frank Pfenning. TCS, 290(2):1175-1199, 2003.

Type Assignment for Intersections and Unions in Call-by-Value LanguagesJoshua Dunfield, Frank Pfenning. fossacs 2003: 250-266 [doi]

A modal foundation for meta-variablesAleksandar Nanevski, Brigitte Pientka, Frank Pfenning. ICFP 2003: [doi]

A type theory for memory allocation and data layoutLeaf Petersen, Robert Harper, Karl Crary, Frank Pfenning. POPL 2003: 172-184 [doi]

Generative Programming and Component Engineering, Second International Conference, GPCE 2003, Erfurt, Germany, September 22-25, 2003, ProceedingsFrank Pfenning, Yannis Smaragdakis, editors, Volume 2830 of Lecture Notes in Computer Science, Springer, 2003.

A Coverage Checking Algorithm for LFCarsten Schürmann, Frank Pfenning. tphol 2003: 120-135 [doi]

A Learning Algorithm for Localizing People Based on Wireless Signal Strength that Uses Labeled and Unlabeled DataSebastian Thrun, Geoffrey J. Gordon, Frank Pfenning, Mary Berna, Brennan Sellner, Brad Lisien. IJCAI 2003: 1427-1428

A Concurrent Logical Framework: The Propositional FragmentKevin Watkins, Iliano Cervesato, Frank Pfenning, David Walker. TYPES 2004: 355-377 [doi]

2002

EditorialMartín Abadi, Leonid Libkin, Frank Pfenning. tocl, 3(3):335-335, 2002. [doi]

A Linear Logical FrameworkIliano Cervesato, Frank Pfenning. iandc, 179(1):19-75, 2002. [doi]

Trustless Grid Computing in ConCertBor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, Frank Pfenning. ccgrid 2002: 112-125 [doi]

PrefaceFrank Pfenning. ENTCS, 70(2), 2002. [doi]

Invited talk: Tri-Directional Type CheckingFrank Pfenning. ENTCS, 70(1), 2002. [doi]

2001

A modal analysis of staged computationRowan Davies, Frank Pfenning. JACM, 48(3):555-604, 2001. [doi]

Logical FrameworksFrank Pfenning. In John Alan Robinson, Andrei Voronkov, editors, Handbook of Automated Reasoning (in 2 volumes). pages 1063-1147, Elsevier and MIT Press, 2001.

A judgmental reconstruction of modal logicFrank Pfenning, Rowan Davies. mscs, 11(4):511-540, 2001.

Primitive recursion for higher-order abstract syntaxCarsten Schürmann, Joëlle Despeyroux, Frank Pfenning. TCS, 266(1-2):1-57, 2001. [doi]

2000

Intersection types and computational effectsRowan Davies, Frank Pfenning. ICFP 2000: 198-208 [doi]

Editorial: Strategies in Automated DeductionBernhard Gramlich, Hélène Kirchner, Frank Pfenning. AMAI, 29(1-4), 2000.

On the Logical Foundations of Staged Computation (Abstract of Invited Talk)Frank Pfenning. PEPM 2000: 33 [doi]

1999

On proving syntactic properties of CPS programsOlivier Danvy, Belmina Dzafic, Frank Pfenning. ENTCS, 26, 1999. [doi]

The Relative Complement Problem for Higher-Order PatternsAlberto Momigliano, Frank Pfenning. agp 1999: 497-512

The Relative Complement Problem for Higher-Order PatternsAlberto Momigliano, Frank Pfenning. ICLP 1999: 380-394

System Description: Twelf - A Meta-Logical Framework for Deductive SystemsFrank Pfenning, Carsten Schürmann. cade 1999: 202-206 [doi]

Logical and Meta-Logical Frameworks (Abstract)Frank Pfenning. ppdp 1999: 206

Natural Deduction for Intuitionistic Non-communicative Linear LogicJeff Polakow, Frank Pfenning. tlca 1999: 295-309 [doi]

Relating Natural Deduction and Sequent Calculus for Intuitionistic Non-Commutative Linear LogicJ. Polokow, Frank Pfenning. ENTCS, 20, 1999. [doi]

Dependent Types in Practical ProgrammingHongwei Xi, Frank Pfenning. POPL 1999: 214-227 [doi]

1998

1997

Linear Higher-Order Pre-UnificationIliano Cervesato, Frank Pfenning. lics 1997: 422-433 [doi]

Primitive Recursion for Higher-Order Abstract SyntaxJoëlle Despeyroux, Frank Pfenning, Carsten Schürmann. tlca 1997: 147-163

On the Unification Problem for Cartesian Closed CategoriesPaliath Narendran, Frank Pfenning, Richard Statman. JSYML, 62(2):636-647, 1997.

1996

1995

Structural Cut EliminationFrank Pfenning. lics 1995: 156-166

On a modal lambda calculus for S4Frank Pfenning, Hao Chi Wong. ENTCS, 1, 1995. [doi]

1994

Logic Programming and Automated Reasoning, 5th International Conference, LPAR 94, Kiev, Ukraine, July 16-22, 1994, ProceedingsFrank Pfenning, editor, Volume 822 of Lecture Notes in Computer Science, Springer, 1994.

Elf: A Meta-Language for Deductive Systems (System Descrition)Frank Pfenning. cade 1994: 811-815

1993

1992

Higher-Order and Modal Logic as a Framework for Explanation-Based GeneralizationScott Dietzen, Frank Pfenning. ml, 9:23-55, 1992.

The Type System of a Higher-Order Logic Programming LanguageGopalan Nadathur, Frank Pfenning. In Types in Logic Programming. pages 245-283, 1992.

Implementing the Meta-Theory of Deductive SystemsFrank Pfenning, Ekkehard Rohwedder. cade 1992: 537-551

1991

A Declarative Alternative to Assert in Logic ProgrammingScott Dietzen, Frank Pfenning. slp 1991: 372-386

Compiling the Polymorphic Lambda-CalculusSpiro Michaylov, Frank Pfenning. PEPM 1991: 285-296

Natural Semantics and Some of Its Meta-Theory in ElfSpiro Michaylov, Frank Pfenning. elp 1992: 299-344

Metacircularity in the Polymorphic lambda-CalculusFrank Pfenning, Peter Lee. TCS, 89(1):137-159, 1991.

1990

Tutorial on Lambda-PrologAmy P. Felty, Elsa L. Gunter, Dale Miller, Frank Pfenning. cade 1990: 682

Presenting Intuitive Deductions via Symmetric SimplificationFrank Pfenning, Dan Nesmith. cade 1990: 336-350

Types in Logic ProgrammingFrank Pfenning. ICLP 1990: 786

1989

Higher-Order and Modal Logic as a Framework for Explanation-Based GeneralizationScott Dietzen, Frank Pfenning. icml 1989: 447-449

Inductively Defined Types in the Calculus of ConstructionsFrank Pfenning, Christine Paulin-Mohring. mfps 1990: 209-228

LEAP: A Language with Eval And PolymorphismFrank Pfenning, Peter Lee. tapsoft 1989: 345-359

Elf: A Language for Logic Definition and Verified MetaprogrammingFrank Pfenning. lics 1989: 313-322

1988

1986

The TPS Theorem Proving SystemPeter B. Andrews, Frank Pfenning, Sunil Issar, C. P. Klapper. cade 1986: 663-664

1984

Analytic and Non-analytic ProofsFrank Pfenning. cade 1984: 394-413