×

zbMATH — the first resource for mathematics

Pfenning, Frank

Compute Distance To:
Author ID: pfenning.frank Recent zbMATH articles by "Pfenning, Frank"
Published as: Pfenning, Frank; Pfenning, F.
External Links: MGP · Wikidata
Documents Indexed: 91 Publications since 1984, including 6 Books

Publications by Year

Citations contained in zbMATH Open

69 Publications have been cited 626 times in 388 Documents Cited by Year
Uniform proofs as a foundation for logic programming. Zbl 0721.03037
Miller, Dale; Nadathur, Gopalan; Pfenning, Frank; Scedrov, Andre
87
1991
A judgmental reconstruction of modal logic. Zbl 0997.03020
Pfenning, Frank; Davies, Rowan
47
2001
A modal analysis of staged computation. Zbl 1323.68107
Davies, Rowan; Pfenning, Frank
46
2001
Session types as intuitionistic linear propositions. Zbl 1287.68125
Caires, Luís; Pfenning, Frank
36
2010
A concurrent logical framework: The propositional fragment. Zbl 1100.68548
Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David
31
2004
Contextual modal type theory. Zbl 1367.03060
Nanevski, Aleksandar; Pfenning, Frank; Pientka, Brigitte
28
2008
Logic programming in the LF logical framework. Zbl 0760.68014
Pfenning, Frank
22
1991
A linear logical framework. Zbl 1031.03056
Cervesato, Iliano; Pfenning, Frank
21
2002
Logical frameworks. Zbl 0992.03038
Pfenning, Frank
18
2001
Structural cut elimination. I: Intuitionistic and classical logic. Zbl 1005.03049
Pfenning, Frank
14
2000
On equivalence and canonical forms in the LF type theory. Zbl 1367.03055
Harper, Robert; Pfenning, Frank
13
2005
TPS: A theorem-proving system for classical type theory. Zbl 0858.03017
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei
13
1996
A logical characterization of forward and backward chaining in the inverse method. Zbl 1151.03006
Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg
13
2008
Elf: A language for logic definition and verified metaprogramming. Zbl 0716.68079
Pfenning, Frank
11
1989
A probabilistic language based upon sampling functions. Zbl 1369.68083
Park, Sungwoo; Pfenning, Frank; Thrun, Sebastian
10
2005
Linear logic propositions as session types. Zbl 1361.68162
Caires, Luís; Pfenning, Frank; Toninho, Bernardo
9
2016
Proof-carrying code in a session-typed process calculus. Zbl 1350.68204
Pfenning, Frank; Caires, Luis; Toninho, Bernardo
9
2011
A linear spine calculus. Zbl 1041.03007
Cervesato, Iliano; Pfenning, Frank
9
2003
Primitive recursion for higher-order abstract syntax. Zbl 0994.68028
Schürmann, C.; Despeyroux, J.; Pfenning, F.
9
2001
Intersection types and computational effects. Zbl 1321.68147
Davies, Rowan; Pfenning, Frank
8
2000
Primitive recursion for higher-order abstract syntax. Zbl 1063.03511
Despeyroux, Joëlle; Pfenning, Frank; Schürmann, Carsten
8
1997
A coverage checking algorithm for LF. Zbl 1279.68295
Schürmann, Carsten; Pfenning, Frank
8
2003
Behavioral polymorphism and parametricity in session-based communication. Zbl 1381.68197
Caires, Luís; Pérez, Jorge A.; Pfenning, Frank; Toninho, Bernardo
8
2013
Higher-order processes, functions, and sessions: a monadic integration. Zbl 1381.68063
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
8
2013
Staged computation with names and necessity. Zbl 1085.68025
Nanevski, Aleksandar; Pfenning, Frank
7
2005
On the undecidability of partial polymorphic type reconstruction. Zbl 0789.03017
Pfenning, Frank
7
1993
Automating higher-order logic. Zbl 0551.68075
Andrews, Peter B.; Miller, Dale A.; Cohen, Eve Longini; Pfenning, Frank
7
1984
Tridirectional typechecking. Zbl 1325.68062
Dunfield, Joshua; Pfenning, Frank
6
2004
On a modal lambda calculus for S4. Zbl 0908.03018
Pfenning, Frank; Wong, Hao-Chi
6
1995
Linear logical relations for session-based concurrency. Zbl 1352.68189
Pérez, Jorge A.; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
6
2012
Linear logical relations and observational equivalences for session-based concurrency. Zbl 1309.68141
Pérez, Jorge A.; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
6
2014
Algorithms for equality and unification in the presence of notational definitions. Zbl 0942.03014
Pfenning, Frank; Schürmann, Carsten
5
1999
On the unification problem for Cartesian closed categories. Zbl 0882.03044
Narendran, Paliath; Pfenning, Frank; Statman, Richard
5
1997
Analytic and non-analytic proofs. Zbl 0547.03032
Pfenning, Frank
5
1984
Automated theorem proving in a simple meta-logic for LF. Zbl 0924.03024
Schürmann, Carsten; Pfenning, Frank
5
1998
Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. Zbl 1182.68212
McLaughlin, Sean; Pfenning, Frank
5
2008
Monitors and blame assignment for higher-order session types. Zbl 1347.68269
Jia, Limin; Gommerstadt, Hannah; Pfenning, Frank
4
2016
Efficient resource management for linear logic proof search. Zbl 0958.03010
Cervesato, Iliano; Hodas, Joshua S.; Pfenning, Frank
4
2000
Metacircularity in the polymorphic \(\lambda\)-calculus. Zbl 0736.03003
Pfenning, Frank; Lee, Peter
4
1991
Implementing the meta-theory of deductive systems. Zbl 0925.03062
Pfenning, Frank; Rohwedder, Ekkehard
4
1992
Cut reduction in linear logic as asynchronous session-typed communication. Zbl 1252.03141
DeYoung, Henry; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
4
2012
On proving syntactic properties of CPS programs. Zbl 0958.68022
Danvy, Olivier; Dzafic, Belmina; Pfenning, Frank
3
1999
Type assignment for intersections and unions in call-by-value languages. Zbl 1029.68098
Dunfield, Joshua; Pfenning, Frank
3
2003
Polarized substructural session types. Zbl 1459.68042
Pfenning, Frank; Griffith, Dennis
3
2015
A monadic analysis of information flow security with mutable state. Zbl 1077.68019
Crary, Karl; Kliger, Aleksey; Pfenning, Frank
3
2005
Natural deduction for intuitionistic non-commutative linear logic. Zbl 0931.03071
Polakow, Jeff; Pfenning, Frank
3
1999
Optimizing higher-order pattern unification. Zbl 1278.68278
Pientka, Brigitte; Pfenning, Frank
3
2003
TPS: A theorem proving system for classical type theory. Zbl 1226.03026
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei
3
2008
Efficient intuitionistic theorem proving with the polarized inverse method. Zbl 1250.03019
McLaughlin, Sean; Pfenning, Frank
3
2009
A module system for a programming language based on the LF logical framework. Zbl 0902.68031
Harper, Robert; Pfenning, Frank
2
1998
Logical frameworks – a brief introduction. Zbl 1097.68541
Pfenning, Frank
2
2002
Linear logical algorithms. Zbl 1155.68349
Simmons, Robert J.; Pfenning, Frank
2
2008
Focusing the inverse method for linear logic. Zbl 1136.03338
Chaudhuri, Kaustuv; Pfenning, Frank
2
2005
Refinement types as proof irrelevance. Zbl 1202.68107
Lovas, William; Pfenning, Frank
2
2009
Logical approximation for program analysis. Zbl 1256.68045
Simmons, Robert J.; Pfenning, Frank
2
2011
Corecursion and non-divergence in session-typed processes. Zbl 1444.68124
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
1
2014
Higher-order pattern complement and the strict \(\lambda\)-calculus. Zbl 1365.68155
Momigliano, Alberto; Pfenning, Frank
1
2003
Reasoning about staged computation (abstract of invited talk). Zbl 1044.68555
Pfenning, Frank
1
2000
Program development through proof transformation. Zbl 0692.68010
Pfenning, Frank
1
1990
A type theory for memory allocation and data layout. Zbl 1321.68181
Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank
1
2003
Intuitionistic letcc via labelled deduction. Zbl 1347.03061
Reed, Jason; Pfenning, Frank
1
2009
Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. Zbl 0926.03076
Polakow, Jeff; Pfenning, Frank
1
1999
A focusing inverse method theorem prover for first-order linear logic. Zbl 1135.68554
Chaudhuri, Kaustuv; Pfenning, Frank
1
2005
Functions as session-typed processes. Zbl 1352.68191
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
1
2012
Church and Curry: combining intrinsic and extrinsic typing. Zbl 1226.03020
Pfenning, Frank
1
2008
A logical characterization of forward and backward chaining in the inverse method. Zbl 1222.68358
Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg
1
2006
Refinement types for logical frameworks and their interpretation as proof irrelevance. Zbl 1202.68108
Lovas, William; Pfenning, Frank
1
2010
Specifying properties of concurrent computations in CLF. Zbl 1278.03069
Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David
1
2007
A bidirectional refinement type system for LF. Zbl 1278.03060
Lovas, William; Pfenning, Frank
1
2008
Linear logic propositions as session types. Zbl 1361.68162
Caires, Luís; Pfenning, Frank; Toninho, Bernardo
9
2016
Monitors and blame assignment for higher-order session types. Zbl 1347.68269
Jia, Limin; Gommerstadt, Hannah; Pfenning, Frank
4
2016
Polarized substructural session types. Zbl 1459.68042
Pfenning, Frank; Griffith, Dennis
3
2015
Linear logical relations and observational equivalences for session-based concurrency. Zbl 1309.68141
Pérez, Jorge A.; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
6
2014
Corecursion and non-divergence in session-typed processes. Zbl 1444.68124
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
1
2014
Behavioral polymorphism and parametricity in session-based communication. Zbl 1381.68197
Caires, Luís; Pérez, Jorge A.; Pfenning, Frank; Toninho, Bernardo
8
2013
Higher-order processes, functions, and sessions: a monadic integration. Zbl 1381.68063
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
8
2013
Linear logical relations for session-based concurrency. Zbl 1352.68189
Pérez, Jorge A.; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
6
2012
Cut reduction in linear logic as asynchronous session-typed communication. Zbl 1252.03141
DeYoung, Henry; Caires, Luís; Pfenning, Frank; Toninho, Bernardo
4
2012
Functions as session-typed processes. Zbl 1352.68191
Toninho, Bernardo; Caires, Luis; Pfenning, Frank
1
2012
Proof-carrying code in a session-typed process calculus. Zbl 1350.68204
Pfenning, Frank; Caires, Luis; Toninho, Bernardo
9
2011
Logical approximation for program analysis. Zbl 1256.68045
Simmons, Robert J.; Pfenning, Frank
2
2011
Session types as intuitionistic linear propositions. Zbl 1287.68125
Caires, Luís; Pfenning, Frank
36
2010
Refinement types for logical frameworks and their interpretation as proof irrelevance. Zbl 1202.68108
Lovas, William; Pfenning, Frank
1
2010
Efficient intuitionistic theorem proving with the polarized inverse method. Zbl 1250.03019
McLaughlin, Sean; Pfenning, Frank
3
2009
Refinement types as proof irrelevance. Zbl 1202.68107
Lovas, William; Pfenning, Frank
2
2009
Intuitionistic letcc via labelled deduction. Zbl 1347.03061
Reed, Jason; Pfenning, Frank
1
2009
Contextual modal type theory. Zbl 1367.03060
Nanevski, Aleksandar; Pfenning, Frank; Pientka, Brigitte
28
2008
A logical characterization of forward and backward chaining in the inverse method. Zbl 1151.03006
Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg
13
2008
Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. Zbl 1182.68212
McLaughlin, Sean; Pfenning, Frank
5
2008
TPS: A theorem proving system for classical type theory. Zbl 1226.03026
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei
3
2008
Linear logical algorithms. Zbl 1155.68349
Simmons, Robert J.; Pfenning, Frank
2
2008
Church and Curry: combining intrinsic and extrinsic typing. Zbl 1226.03020
Pfenning, Frank
1
2008
A bidirectional refinement type system for LF. Zbl 1278.03060
Lovas, William; Pfenning, Frank
1
2008
Specifying properties of concurrent computations in CLF. Zbl 1278.03069
Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David
1
2007
A logical characterization of forward and backward chaining in the inverse method. Zbl 1222.68358
Chaudhuri, Kaustuv; Pfenning, Frank; Price, Greg
1
2006
On equivalence and canonical forms in the LF type theory. Zbl 1367.03055
Harper, Robert; Pfenning, Frank
13
2005
A probabilistic language based upon sampling functions. Zbl 1369.68083
Park, Sungwoo; Pfenning, Frank; Thrun, Sebastian
10
2005
Staged computation with names and necessity. Zbl 1085.68025
Nanevski, Aleksandar; Pfenning, Frank
7
2005
A monadic analysis of information flow security with mutable state. Zbl 1077.68019
Crary, Karl; Kliger, Aleksey; Pfenning, Frank
3
2005
Focusing the inverse method for linear logic. Zbl 1136.03338
Chaudhuri, Kaustuv; Pfenning, Frank
2
2005
A focusing inverse method theorem prover for first-order linear logic. Zbl 1135.68554
Chaudhuri, Kaustuv; Pfenning, Frank
1
2005
A concurrent logical framework: The propositional fragment. Zbl 1100.68548
Watkins, Kevin; Cervesato, Iliano; Pfenning, Frank; Walker, David
31
2004
Tridirectional typechecking. Zbl 1325.68062
Dunfield, Joshua; Pfenning, Frank
6
2004
A linear spine calculus. Zbl 1041.03007
Cervesato, Iliano; Pfenning, Frank
9
2003
A coverage checking algorithm for LF. Zbl 1279.68295
Schürmann, Carsten; Pfenning, Frank
8
2003
Type assignment for intersections and unions in call-by-value languages. Zbl 1029.68098
Dunfield, Joshua; Pfenning, Frank
3
2003
Optimizing higher-order pattern unification. Zbl 1278.68278
Pientka, Brigitte; Pfenning, Frank
3
2003
Higher-order pattern complement and the strict \(\lambda\)-calculus. Zbl 1365.68155
Momigliano, Alberto; Pfenning, Frank
1
2003
A type theory for memory allocation and data layout. Zbl 1321.68181
Petersen, Leaf; Harper, Robert; Crary, Karl; Pfenning, Frank
1
2003
A linear logical framework. Zbl 1031.03056
Cervesato, Iliano; Pfenning, Frank
21
2002
Logical frameworks – a brief introduction. Zbl 1097.68541
Pfenning, Frank
2
2002
A judgmental reconstruction of modal logic. Zbl 0997.03020
Pfenning, Frank; Davies, Rowan
47
2001
A modal analysis of staged computation. Zbl 1323.68107
Davies, Rowan; Pfenning, Frank
46
2001
Logical frameworks. Zbl 0992.03038
Pfenning, Frank
18
2001
Primitive recursion for higher-order abstract syntax. Zbl 0994.68028
Schürmann, C.; Despeyroux, J.; Pfenning, F.
9
2001
Structural cut elimination. I: Intuitionistic and classical logic. Zbl 1005.03049
Pfenning, Frank
14
2000
Intersection types and computational effects. Zbl 1321.68147
Davies, Rowan; Pfenning, Frank
8
2000
Efficient resource management for linear logic proof search. Zbl 0958.03010
Cervesato, Iliano; Hodas, Joshua S.; Pfenning, Frank
4
2000
Reasoning about staged computation (abstract of invited talk). Zbl 1044.68555
Pfenning, Frank
1
2000
Algorithms for equality and unification in the presence of notational definitions. Zbl 0942.03014
Pfenning, Frank; Schürmann, Carsten
5
1999
On proving syntactic properties of CPS programs. Zbl 0958.68022
Danvy, Olivier; Dzafic, Belmina; Pfenning, Frank
3
1999
Natural deduction for intuitionistic non-commutative linear logic. Zbl 0931.03071
Polakow, Jeff; Pfenning, Frank
3
1999
Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. Zbl 0926.03076
Polakow, Jeff; Pfenning, Frank
1
1999
Automated theorem proving in a simple meta-logic for LF. Zbl 0924.03024
Schürmann, Carsten; Pfenning, Frank
5
1998
A module system for a programming language based on the LF logical framework. Zbl 0902.68031
Harper, Robert; Pfenning, Frank
2
1998
Primitive recursion for higher-order abstract syntax. Zbl 1063.03511
Despeyroux, Joëlle; Pfenning, Frank; Schürmann, Carsten
8
1997
On the unification problem for Cartesian closed categories. Zbl 0882.03044
Narendran, Paliath; Pfenning, Frank; Statman, Richard
5
1997
TPS: A theorem-proving system for classical type theory. Zbl 0858.03017
Andrews, Peter B.; Bishop, Matthew; Issar, Sunil; Nesmith, Dan; Pfenning, Frank; Xi, Hongwei
13
1996
On a modal lambda calculus for S4. Zbl 0908.03018
Pfenning, Frank; Wong, Hao-Chi
6
1995
On the undecidability of partial polymorphic type reconstruction. Zbl 0789.03017
Pfenning, Frank
7
1993
Implementing the meta-theory of deductive systems. Zbl 0925.03062
Pfenning, Frank; Rohwedder, Ekkehard
4
1992
Uniform proofs as a foundation for logic programming. Zbl 0721.03037
Miller, Dale; Nadathur, Gopalan; Pfenning, Frank; Scedrov, Andre
87
1991
Logic programming in the LF logical framework. Zbl 0760.68014
Pfenning, Frank
22
1991
Metacircularity in the polymorphic \(\lambda\)-calculus. Zbl 0736.03003
Pfenning, Frank; Lee, Peter
4
1991
Program development through proof transformation. Zbl 0692.68010
Pfenning, Frank
1
1990
Elf: A language for logic definition and verified metaprogramming. Zbl 0716.68079
Pfenning, Frank
11
1989
Automating higher-order logic. Zbl 0551.68075
Andrews, Peter B.; Miller, Dale A.; Cohen, Eve Longini; Pfenning, Frank
7
1984
Analytic and non-analytic proofs. Zbl 0547.03032
Pfenning, Frank
5
1984
all top 5

Cited by 493 Authors

17 Pfenning, Frank
15 Miller, Dale Allen
14 Pientka, Brigitte
9 Francez, Nissim
8 Cervesato, Iliano
8 Rabe, Florian
8 Yoshida, Nobuko
7 Felty, Amy P.
7 Nadathur, Gopalan
7 Olarte, Carlos
7 Pym, David J.
6 Abel, Andreas M.
6 Momigliano, Alberto
6 Pérez, Jorge A.
6 Pimentel, Elaine
6 Toninho, Bernardo
5 Caires, Luís
5 Chaudhuri, Kaustuv
5 Honsell, Furio
5 Horozal, Fulya
5 Liquori, Luigi
5 Nigam, Vivek
5 Schürmann, Carsten
4 Andrews, Peter B.
4 Benzmüller, Christoph Ewald
4 Cheney, James
4 Fujita, Ken-etsu
4 Harper, Robert
4 Licata, Daniel R.
4 Lipton, James B.
4 Pitts, Andrew M.
4 Ritter, Eike
4 Stump, Aaron
3 Atkey, Robert
3 Birkedal, Lars
3 Bonelli, Eduardo
3 del Carmen González Huesca, Lourdes
3 Dunfield, Joshua
3 Dyckhoff, Roy
3 Gabbay, Murdoch James
3 Gacek, Andrew
3 Galmiche, Didier
3 Kiselyov, Oleg
3 Kohlhase, Michael
3 Komendantskaya, Ekaterina
3 Miculan, Marino
3 Miranda Perea, Favio Ezequiel
3 Montesi, Fabrizio
3 Narendran, Paliath
3 Park, Sungwoo
3 Paulson, Lawrence Charles
3 Ruet, Paul
3 Scedrov, Andre
3 Schubert, Aleksy
3 Shulman, Michael A.
3 Simmons, Robert jun.
3 Straßburger, Lutz
3 Vestergaard, René
3 Wallen, Lincoln A.
3 Zeilberger, Noam
2 Acar, Umut A.
2 Amato, Gianluca
2 Anantharaman, Siva
2 Anderson, Penny
2 Andreoli, Jean-Marc
2 Artemov, Sergei
2 Bartoletti, Massimo
2 Bishop, Matthew
2 Blanchette, Jasmin Christian
2 Brock-Nannestad, Taus
2 Brotherston, James
2 Brown, Chad Edward
2 Carbone, Marco
2 Cave, Andrew
2 Chihani, Zakaria
2 Ciabattoni, Agata
2 Clouston, Ranald A.
2 Crary, Karl
2 Dal Lago, Ugo
2 Danvy, Olivier
2 Deng, Yuxin
2 Despeyroux, Joëlle
2 Dezani-Ciancaglini, Mariangiola
2 Dixon, Lucas
2 Duggan, Dominic
2 Farmer, William M.
2 Feller, Federico
2 Francalanza, Adrian
2 Fu, Peng
2 Ghilezan, Silvia
2 Giannini, Paola
2 Honda, Kohei
2 Horne, Ross
2 Igarashi, Atsushi
2 Im, Hyeonseung
2 Kameyama, Yukiyoshi
2 Kamide, Norihiro
2 Kavvos, G. A.
2 Kesner, Delia
2 Kobayashi, Naoki
...and 393 more Authors

Citations by Year

Wikidata Timeline

The data are displayed as stored in Wikidata under a Creative Commons CC0 License. Updates and corrections should be made in Wikidata.