search ~fp
Home
Contact Information
Curriculum Vitæ
Research Interests
Publications
DBLP
Google Scholar Search
Google Scholar Profile
Students & Co-authors
Projects
MetaCLF
C0
Certified Interfaces
Prospero
Manifest Security
Twelf
Courses
Logic Programming [Fa06]
Computer Systems [Sp06]
Computer Systems [Sp05]
Prog. Langs. [Fa04]
Theorem Proving [Sp04]
Prog. Langs. [Fa03]
Computer Graphics [Sp03]
Prog. Langs. [Fa02]
Computer Graphics [Sp02]
Linear Logic [Fa01]
Comp. & Ded. [Sp01]
Summer School
Oregon'10
Oregon'11
Conferences
IJCAR'12
LFMTP'12
Turing 100
ITRS'12
Organizations
Journals
CMU Squash Ladder
 
Frank Pfenning
  

Frank Pfenning
Bibliography

The bibliography is sorted by publication type, in reverse chronological order in each category. Links to PDF files are given where available. My publications could be more up-to-date, or check my home page for most recent drafts and publications.

Last Updated: Sat May 29, 2010

Contents Books | Book Chapters
Journals: Published | Accepted | Submitted
Conferences and Workshops: Refereed | Unrefereed
Technical Reports | Other Publications
Elsewhere Publications | BibTeX Source

    Books

  1. F. Pfenning, editor. Proceedings of the 23rd Annual Symposium on Logic in Computer Science (LICS 2008), Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society Press.

  2. F. Pfenning, editor. Proceedings of the 21st International Conference on Automated Deduction (CADE-21), Bremen, Germany, July 2007. Springer LNCS 4603.

  3. Frank Pfenning, editor. Proceedings of the 17th International Conference on Rewriting Techniques and Applications, Seattle, Washington, August 2006. Springer Verlag LNCS 4098.

  4. Frank Pfenning. Computation and Deduction. Cambridge University Press. In preparation. Draft from April 1997 available electronically. Available electronically

  5. Frank Pfenning and Yannis Smaragdakis, editors. Proceedings of the Second International Conference on Generative Programming and Component Engineering. Springer-Verlag LNCS 2830, Erfurt, Germany, September 2003.

  6. Frank Pfenning, editor. Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages (LFM'02), volume 70(2) of Electronic Notes in Theoretical Computer Science, Copenhagen, Denmark, July 2002. Available electronically

  7. Maurizio Gabrielli and Frank Pfenning, editors. Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP'00), Ottawa, Canada, September 2000. ACM Press.

  8. Frank Pfenning, editor. Logic Programming and Automated Reasoning, 5th International Conference, LPAR'94, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.

  9. Frank Pfenning, editor. Types in Logic Programming. MIT Press, Cambridge, Massachusetts, 1992.

    Book Chapters

  10. Frank Pfenning. Church and Curry: Combining intrinsic and extrinsic typing. In C.Benzmüller, C.Brown, J.Siekmann, and R.Statman, editors, Reasoning in Simple Type Theory: Festschrift in Honor of Peter B. Andrews on His 70th Birthday, Studies in Logic 17, pages 303-338. College Publications, 2008. [PDF]

  11. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework: The propositional fragment. In S. Berardi, M. Coppo, and F. Damiani, editors, Types for Proofs and Programs, pages 355-377. Springer-Verlag LNCS 3085, 2004. Revised selected papers from the Third International Workshop on Types for Proofs and Programs, Torino, Italy, April 2003. [PDF]

  12. Frank Pfenning. Logical frameworks - a brief introduction. In H. Schwichtenberg and R. Steinbrüggen, editors, Proof and System-Reliability, volume 62 of NATO Science Series II, pages 137-166. Kluwer Academic Publishers, 2002. Lecture notes from the Marktoberdorf Summer School, July 2001. [PDF]

  13. Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, chapter 17, pages 1063-1147. Elsevier Science and MIT Press, 2001. [PDF]

  14. Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In T. Altenkirch, W. Naraschewski, and B. Reus, editors, Types for Proofs and Programs, pages 179-193, Kloster Irsee, Germany, March 1998. Springer-Verlag LNCS 1657. [PDF]

  15. Gopalan Nadathur and Frank Pfenning. The type system of a higher-order logic programming language. In Frank Pfenning, editor, Types in Logic Programming, pages 245-283. MIT Press, 1992.

  16. Frank Pfenning. Dependent types in logic programming. In Frank Pfenning, editor, Types in Logic Programming, chapter 10, pages 285-311. MIT Press, Cambridge, Massachusetts, 1992.

  17. Frank Pfenning. Logic programming in the LF logical framework. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149-181. Cambridge University Press, 1991. [PDF]

  18. Conal Elliott and Frank Pfenning. A semi-functional implementation of a higher-order logic programming language. In Peter Lee, editor, Topics in Advanced Language Implementation, pages 289-325. MIT Press, 1991. Available electronically

    Journal Papers - Published

  19. Aleksandar Nanevski, Frank Pfenning, and Brigitte Pientka. Contextual modal type theory. Transactions on Computational Logic, 9(3), 2008. [PDF]

  20. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. Transactions on Programming Languages and Systems, 31(1), December 2008. [PDF]

  21. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. Journal of Automated Reasoning, 40(2-3):133-177, 2008. Special issue with selected papers from IJCAR 2006. [PDF]

  22. Aleksandar Nanevski and Frank Pfenning. Staged computation with names and necessity. Journal of Functional Programming, 15(6):837-891, November 2005. [PDF]

  23. Karl Crary, Aleksey Kliger, and Frank Pfenning. A monadic analysis of information flow security with mutable state. Journal of Functional Programming, 15(2):249-291, March 2005. Preliminary version available as Technical Report CMU-CS-03-164. [PDF]

  24. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Transactions on Computational Logic, 6:61-101, January 2005. [PDF]

  25. Peter B. Andrews, Matthew Bishop, Chad E. Brown, Sunil Issar, Frank Pfenning, and Hongwei Xi. ETPS: A system to help students write formal proofs. Journal of Automated Reasoning, 32(1):75-92, 2004. Available electronically

  26. Alberto Momigliano and Frank Pfenning. Higher-order pattern complement and the strict lambda-calculus. Transactions on Computational Logic, 4(4), October 2003. [PDF]

  27. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Journal of Logic and Computation, 13(5):639-688, 2003.

  28. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provable safe mobile code. Theoretical Computer Science, 290:1175-1199, 2003. Special issue on Dependable Computing. Preliminary version appeared in the proceedings of the DARPA Information Survivability Conference and Exposition (DISCEX 2000), vol 1, pp. 406-419, Hilton Head Island, South Carolina, January 2000. [PDF]

  29. Iliano Cervesato and Frank Pfenning. A linear logical framework. Information & Computation, 179(1):19-75, November 2002. Revised and expanded version of an extended abstract, LICS 1996, pp. 264-275. [PDF]

  30. Carsten Schürmann, Joëlle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 266:1-57, 2001.

  31. Frank Pfenning and Rowan Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11:511-540, 2001. Notes to an invited talk at the Workshop on Intuitionistic Modal Logics and Applications (IMLA'99), Trento, Italy, July 1999. [PDF]

  32. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Journal of the ACM, 48(3):555-604, May 2001. [PDF]

  33. Frank Pfenning. Structural cut elimination I. Intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. [PDF]

  34. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 232(1-2):133-163, February 2000. Special issue on Proof Search in Type-Theoretic Languages, D. Galmiche and D. Pym, editors. [PDF]

  35. Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for run-time code generation. ACM Computing Surveys, 30(3es), September 1998. [PDF]

  36. Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Journal of Logic and Computation, 8(1):5-31, 1998.

  37. Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for Cartesian closed categories. Journal of Symbolic Logic, 62(2):636-647, 1997.

  38. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: A theorem proving system for classical type theory. Journal of Automated Reasoning, 16(3):321-353, June 1996.

  39. Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1,2):185-199, 1993. Preliminary version available as Technical Report CMU-CS-92-105, School of Computer Science, Carnegie Mellon University, January 1992. [PDF]

  40. Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. Machine Learning, 9:23-55, 1992.

  41. Frank Pfenning and Peter Lee. Metacircularity in the polymorphic lambda-calculus. Theoretical Computer Science, 89:137-159, 1991.

  42. Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991.

  43. Frank Pfenning. Program development through proof transformation. Contemporary Mathematics, 106:251-262, 1990. [PDF]

  44. Peter B. Andrews, Dale Miller, Eve Cohen, and Frank Pfenning. Automating higher-order logic. Contemporary Mathematics, 29:169-192, August 1984. [PDF]

    Journal Papers - Accepted

  45. William Lovas and Frank Pfenning. Refinement types for logical frameworks and their interpretation as proof irrelevance. Logical Methods in Computer Science, May 2010. To appear. [PDF]

    Journal Papers - Submitted

  46. Robert J. Simmons and Frank Pfenning. Logical approximation for program analysis. Submitted to the Journal on Higher-Order and Symbolic Computation, March 2010. [PDF]

    Refereed Conference and Workshop Papers

  47. Luís Caires and Frank Pfenning. Session types as intuitionistic linear propositions. In P.Gastin and F.Laroussinie, editors, Proceedings of the 21st International Conference on Concurrency Theory (CONCUR 2010), Paris, France, August 2010. Springer LNCS. To appear. [PDF]

  48. Deepak Garg and Frank Pfenning. A proof-carrying file system. In D.Evans and G.Vigna, editors, Proceedings of the 31st Symposium on Security and Privacy (Oakland 2010), Berkeley, California, May 2010. IEEE. Extended version available as Technical Report CMU-CS-09-123, June 2009. [PDF]

  49. Sean McLaughlin and Frank Pfenning. Efficient intuitionistic theorem proving with the polarized inverse method. In R.A.Schmidt, editor, Proceedings of the 22nd International Conference on Automated Deduction (CADE-22), pages 230-244, Montreal, Canada, August 2009. Springer LNCS 5663. [PDF]

  50. Frank Pfenning and Robert J. Simmons. Substructural operational semantics as ordered logic programming. In Proceedings of the 24th Annual Symposium on Logic in Computer Science (LICS 2009), pages 101-110, Los Angeles, California, August 2009. IEEE Computer Society Press. [PDF]

  51. William Lovas and Frank Pfenning. Refinement types as proof irrelevance. In P.-L. Curien, editor, Proceedings of the 9th International Conference on Typed Lambda Calculi and Applications (TLCA 2009), pages 157-171, Brasilia, Brazil, July 2009. Springer LNCS 5608. [PDF]

  52. Jason Reed and Frank Pfenning. Intuitionistic letcc via labelled deduction. In Proceedings of the 5th Workshop on Methods for Modalities (M4M5 2007), pages 91-111, Cachan, France, November 2007. Electronic Notes in Theoretical Computer Science (ENTCS), vol 213, March 2009. [PDF]

  53. Robert J. Simmons and Frank Pfenning. Linear logical approximations. In G. Puebla and G. Vidal, editors, Proceedings of the Workshop on Partial Evaluation and Program Manipulation, pages 9-20, Savannah, Georgia, January 2009. ACM SIGPLAN. [PDF]

  54. Sean McLaughlin and Frank Pfenning. Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In I.Cervesato, H.Veith, and A.Voronkov, editors, Proceedings of the 15th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'08), pages 174-181, Doha, Qatar, November 2008. Springer LNCS 5330. System Description. [PDF]

  55. Robert J. Simmons and Frank Pfenning. Linear logical algorithms. In Proceedings of the 35th International Colloquium on Automata, Languages and Programming (ICALP'08), pages 336-345, Reykjavik, Iceland, July 2008. Springer LNCS 5126. [PDF]

  56. Henry DeYoung, Deepak Garg, and Frank Pfenning. An authorization logic with explicit time. In Proceedings of the 21st Computer Security Foundations Symposium (CSF-21), pages 133-145, Pittsburgh, Pennsylvania, June 2008. IEEE Computer Society Press. Extended version available as Technical Report CMU-CS-07-166, revised February 2008. [PDF]

  57. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. Specifying properties of concurrent computations in CLF. In C.Schürmann, editor, Proceedings of the 4th International Workshop on Logical Frameworks and Meta-Languages (LFM'04), Cork, Ireland, July 2004. Electronic Notes in Theoretical Computer Science (ENTCS), vol 199, pp. 133-145, 2008. [PDF]

  58. Uluç Saranli and Frank Pfenning. Using constrained intuitionistic linear logic for hybrid robotic planning problems. In Proceedings of the International Conference on Robotics and Automation (ICRA'07), pages 3705-3710, Rome Italy, April 2007. IEEE Computer Society Press. [PDF]

  59. Kevin D. Bowers, Lujo Bauer, Deepak Garg, Frank Pfenning, and Michael K. Reiter. Consumable credentials in logic-based access-control systems. In Proceedings of the 14th Annual Network and Distributed System Security Symposium (NDSS'07), pages 143-157, San Diego, California, February 2007. Internet Society. Preliminary version available as Technical Report CMU-CYLAB-06-002, Carnegie Mellon University, February 2006. [PDF]

  60. Deepak Garg, Lujo Bauer, Kevin Bowers, Frank Pfenning, and Michael Reiter. A linear logic of affirmation and knowledge. In D. Gollman, J. Meier, and A. Sabelfeld, editors, Proceedings of the 11th European Symposium on Research in Computer Security (ESORICS'06), pages 297-312, Hamburg, Germany, September 2006. Springer LNCS 4189. [PDF]

  61. Deepak Garg and Frank Pfenning. Non-interference in constructive authorization logic. In J. Guttman, editor, Proceedings of the 19th Computer Security Foundations Workshop (CSFW'06), pages 283-293, Venice, Italy, July 2006. IEEE Computer Society Press. [PDF]

  62. Kaustuv Chaudhuri, Frank Pfenning, and Greg Price. A logical characterization of forward and backward chaining in the inverse method. In U. Furbach and N. Shankar, editors, Proceedings of the 3rd International Joint Conference on Automated Reasoning (IJCAR'06), pages 97-111, Seattle, Washington, August 2006. Springer LNCS 4130. [PDF]

  63. Kaustuv Chaudhuri and Frank Pfenning. Focusing the inverse method for linear logic. In L.Ong, editor, Proceedings of the 14th Annual Conference on Computer Science Logic (CSL'05), pages 200-215, Oxford, England, August 2005. Springer Verlag LNCS 3634. [PDF]

  64. Deepak Garg and Frank Pfenning. Type-directed concurrency. In M.Abadi and L.de Alfaro, editors, Proceedings of the 16th International Conference on Concurrency Theory (CONCUR'05), pages 6-20, San Francisco, California, August 2005. Springer Verlag LNCS 3653. [PDF]

  65. Kaustuv Chaudhuri and Frank Pfenning. A focusing inverse method prover for first-order linear logic. In R.Nieuwenhuis, editor, Proceedings of the 20th International Conference on Automated Deduction (CADE-20), pages 69-83, Tallinn, Estonia, July 2005. Springer Verlag LNCS 3632. [PDF]

  66. Pablo López, Frank Pfenning, Jeff Polakow, and Kevin Watkins. Monadic concurrent linear logic programming. In A.Felty, editor, Proceedings of the 7th International Symposium on Principles and Practice of Declarative Programming (PPDP'05), pages 35-46, Lisbon, Portugal, July 2005. ACM Press. [PDF]

  67. Sungwoo Park, Frank Pfenning, and Sebastian Thrun. A probabilistic language based upon sampling functions. In M.Abadi, editor, Conference Record of the 32nd Symposium on Principles of Programming Languages (POPL'05), pages 171-182, Long Beach, California, January 2005. ACM Press. [PDF]

  68. Penny Anderson and Frank Pfenning. Verifying uniqueness in a logical framework. In K.Slind, A.Bunker, and G.Gopalakrishnan, editors, Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04), pages 18-33, Park City, Utah, September 2004. Springer LNCS 3223. [PDF]

  69. Tom Murphy VII, Karl Crary, Robert Harper, and Frank Pfenning. A symmetric modal lambda calculus for distributed computing. In H. Ganzinger, editor, Proceedings of the 19th Annual Symposium on Logic in Computer Science (LICS'04), pages 286-295, Turku, Finland, July 2004. IEEE Computer Society Press. Extended version available as Technical Report CMU-CS-04-105. [PDF]

  70. Joshua Dunfield and Frank Pfenning. Tridirectional typechecking. In X.Leroy, editor, Conference Record of the 31st Annual Symposium on Principles of Programming Languages (POPL'04), pages 281-292, Venice, Italy, January 2004. ACM Press. Extended version available as Technical Report CMU-CS-04-117, March 2004. [PDF]

  71. Carsten Schürmann and Frank Pfenning. A coverage checking algorithm for LF. In D. Basin and B. Wolff, editors, Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs 2003), pages 120-135, Rome, Italy, September 2003. Springer-Verlag LNCS 2758. [PDF]

  72. Brigitte Pientka and Frank Pfenning. Optimizing higher-order pattern unification. In F. Baader, editor, Proceedings of the 19th Conference on Automated Deduction (CADE-19), pages 473-487, Miami Beach, Florida, July 2003. Springer-Verlag LNAI 2741. [PDF]

  73. Joshua Dunfield and Frank Pfenning. Type assignment for intersections and unions in call-by-value languages. In A.D. Gordon, editor, Proceedings of the 6th International Conference on Foundations of Software Science and Computation Structures (FOSSACS'03), pages 250-266, Warsaw, Poland, April 2003. Springer-Verlag LNCS 2620. [PDF]

  74. Leaf Petersen, Robert Harper, Karl Crary, and Frank Pfenning. A type theory for memory allocation and data layout. In G. Morrisett, editor, Conference Record of the 30th Annual Symposium on Principles of Programming Languages (POPL'03), pages 172-184, New Orleans, Louisiana, January 2003. ACM Press. Extended version available as Technical Report CMU-CS-02-171, December 2002. [PDF]

  75. Frank Pfenning. Intensionality, extensionality, and proof irrelevance in modal type theory. In J. Halpern, editor, Proceedings of the 16th Annual Symposium on Logic in Computer Science (LICS'01), pages 221-230, Boston, Massachusetts, June 2001. IEEE Computer Society Press. [PDF]

  76. Rowan Davies and Frank Pfenning. Intersection types and computational effects. In P. Wadler, editor, Proceedings of the Fifth International Conference on Functional Programming (ICFP'00), pages 198-208, Montreal, Canada, September 2000. ACM Press. [PDF]

  77. Olivier Danvy, Belmina Dzafic, and Frank Pfenning. On proving syntactic properties of CPS programs. In Andrew Gordon and Andrew Pitts, editors, Proceedings of the Third International Workshop on Higher Order Operational Techniques in Semantics (HOOTS'99), Paris, September 1999. Electronic Notes in Theoretical Computer Science, Volume 26. [PDF] Available electronically

  78. Alberto Momigliano and Frank Pfenning. The relative complement problem for higher-order patterns. In D. De Schreye, editor, Proceedings of the International Conference on Logic Programming (ICLP'99), pages 380-394, Las Cruces, New Mexico, November 1999. MIT Press. [PDF]

  79. Frank Pfenning and Carsten Schürmann. System description: Twelf - a meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the 16th International Conference on Automated Deduction (CADE-16), pages 202-206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. [PDF]

  80. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. [PDF]

  81. Jeff Polakow and Frank Pfenning. Relating natural deduction and sequent calculus for intuitionistic non-commutative linear logic. In Andre Scedrov and Achim Jung, editors, Proceedings of the 15th Conference on Mathematical Foundations of Programming Semantics, pages 449-466, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20. [PDF]

  82. Hongwei Xi and Frank Pfenning. Dependent types in practical programming. In A. Aiken, editor, Conference Record of the 26th Symposium on Principles of Programming Languages (POPL'99), pages 214-227. ACM Press, January 1999. [PDF]

  83. Carsten Schürmann and Frank Pfenning. Automated theorem proving in a simple meta-logic for LF. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. [PDF]

  84. Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation and modal-ML. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 224-235, Montreal, Canada, June 1998. ACM Press. [PDF]

  85. Hongwei Xi and Frank Pfenning. Eliminating array bound checking through dependent types. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 249-257, Montreal, Canada, June 1998. ACM Press. [PDF]

  86. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In Glynn Winskel, editor, Proceedings of the Twelfth Annual Sumposium on Logic in Computer Science (LICS'97), pages 422-433, Warsaw, Poland, June 1997. IEEE Computer Society Press. [PDF]

  87. Joëlle Despeyroux, Frank Pfenning, and Carsten Schürmann. Primitive recursion for higher-order abstract syntax. In R. Hindley, editor, Proceedings of the Third International Conference on Typed Lambda Calculus and Applications (TLCA'97), pages 147-163, Nancy, France, April 1997. Springer-Verlag LNCS 1210. An extended version is available as Technical Report CMU-CS-96-172, Carnegie Mellon University. [PDF]

  88. Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. In M. Maher, editor, Proceedings of the Joint International Conference and Symposium on Logic Programming, pages 259-273, Bonn, Germany, September 1996. MIT Press. [PDF]

  89. Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Eleventh Annual Symposium on Logic in Computer Science, pages 264-275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. [PDF]

  90. Ekkehard Rohwedder and Frank Pfenning. Mode and termination checking for higher-order logic programs. In Hanne Riis Nielson, editor, Proceedings of the European Symposium on Programming, pages 296-310, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1058. [PDF]

  91. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. In R. Dyckhoff, H. Herre, and P. Schroeder-Heister, editors, Proceedings of the 5th International Workshop on Extensions of Logic Programming, pages 67-81, Leipzig, Germany, March 1996. Springer-Verlag LNAI 1050. [PDF]

  92. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. In Guy Steele, Jr., editor, Proceedings of the 23rd Annual Symposium on Principles of Programming Languages, pages 258-270, St. Petersburg Beach, Florida, January 1996. ACM Press. [PDF]

  93. Frank Pfenning. Structural cut elimination. In D. Kozen, editor, Proceedings of the Tenth Annual Symposium on Logic in Computer Science, pages 156-166, San Diego, California, June 1995. IEEE Computer Society Press. [PDF]

  94. Frank Pfenning and Hao-Chi Wong. On a modal lambda-calculus for S4. In S. Brookes and M. Main, editors, Proceedings of the Eleventh Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, March 1995. Electronic Notes in Theoretical Computer Science, Volume 1, Elsevier. [PDF]

  95. Michael Kohlhase and Frank Pfenning. Unification in a lambda-calculus with intersection types. In Dale Miller, editor, Proceedings of the International Logic Programming Symposium, pages 488-505, Vancouver, Canada, October 1993. MIT Press. [PDF]

  96. Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for Cartesian closed categories. In Moshe Vardi, editor, Eighth Annual IEEE Symposium on Logic in Computer Science, pages 57-63, Montreal, Canada, June 1993. [PDF]

  97. John Hannan and Frank Pfenning. Compiler verification in LF. In Andre Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 407-418, Santa Cruz, California, June 1992. [PDF]

  98. Frank Pfenning and Ekkehard Rohwedder. Implementing the meta-theory of deductive systems. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction, pages 537-551, Saratoga Springs, New York, June 1992. Springer-Verlag LNAI 607. [PDF]

  99. Scott Dietzen and Frank Pfenning. A declarative alternative to assert in logic programming. In Vijay Saraswat and Kazunori Ueda, editors, International Logic Programming Symposium, pages 372-386. MIT Press, October 1991. [PDF]

  100. Frank Pfenning. Unification and anti-unification in the Calculus of Constructions. In Sixth Annual IEEE Symposium on Logic in Computer Science, pages 74-85, Amsterdam, The Netherlands, July 1991. [PDF]

  101. Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the SIGPLAN '91 Symposium on Language Design and Implementation, pages 268-277, Toronto, Ontario, June 1991. ACM Press. [PDF]

  102. Spiro Michaylov and Frank Pfenning. Natural semantics and some of its meta-theory in Elf. In L.-H. Eriksson, L. Hallnäs, and P. Schroeder-Heister, editors, Proceedings of the Second International Workshop on Extensions of Logic Programming, pages 299-344, Stockholm, Sweden, January 1991. Springer-Verlag LNAI 596. [PDF]

  103. Spiro Michaylov and Frank Pfenning. Compiling the polymorphic lambda-calculus. In Paul Hudak and Neil Jones, editors, Proceedings of the Symposium on Partial Evaluation and Semantics Based Program Manipulation, pages 285-296, New Haven, Connecticut, June 1991. ACM Press. Published in SIGPLAN Notices 26(9), September 1991.

  104. Frank Pfenning and Daniel Nesmith. Presenting intuitive deductions via symmetric simplification. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 336-350, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. [PDF]

  105. Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. In Alberto Maria Segre, editor, Sixth International Workshop on Machine Learning, pages 447-449, San Mateo, California, June 1989. Morgan Kaufmann Publishers. Expanded version available as Technical Report CMU-CS-89-160, Carnegie Mellon University. [PDF]

  106. Frank Pfenning. Elf: A language for logic definition and verified meta-programming. In Fourth Annual Symposium on Logic in Computer Science, pages 313-322, Pacific Grove, California, June 1989. IEEE Computer Society Press. [PDF]

  107. Frank Pfenning and Peter Lee. LEAP: A language with eval and polymorphism. In Proceedings of the International Joint Conference on Theory and Practice in Software Development, pages 345-359, Barcelona, Spain, March 1989. Springer-Verlag LNCS 352. [PDF]

  108. Frank Pfenning and Christine Paulin-Mohring. Inductively defined types in the Calculus of Constructions. In M. Main, A. Melton, M. Mislove, and D. Schmidt, editors, Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, Tulane University, New Orleans, Louisiana, pages 209-228. Springer-Verlag LNCS 442, March 1989. [PDF]

  109. Robert L. Nord and Frank Pfenning. The Ergo attribute system. In Peter Henderson, editor, Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 110-120. ACM Press, November 1988. [PDF]

  110. Peter Lee, Frank Pfenning, Gene Rollins, and William Scherlis. The Ergo Support System: An integrated set of tools for prototyping integrated environments. In Peter Henderson, editor, Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, pages 25-34. ACM Press, November 1988. [PDF]

  111. Frank Pfenning. Partial polymorphic type inference and higher-order unification. In Proceedings of the 1988 ACM Conference on Lisp and Functional Programming, pages 153-163, Snowbird, Utah, July 1988. ACM Press. [PDF]

  112. Frank Pfenning and Conal Elliott. Higher-order abstract syntax. In Proceedings of the ACM SIGPLAN '88 Symposium on Language Design and Implementation, pages 199-208, Atlanta, Georgia, June 1988. [PDF]

  113. Frank Pfenning. Analytic and non-analytic proofs. In R.E. Shostak, editor, Proceedings of the 7th Conference on Automated Deduction, pages 394-413, Napa, California, May 1984. Springer-Verlag LNCS 170. [PDF]

    Unrefereed Conference and Workshop Papers

  114. Henry DeYoung and Frank Pfenning. Reasoning about the consequences of authorization policies in a linear epistemic logic. In Workshop on Foundations of Computer Security (FCS'09), Los Angeles, California, August 2009. [PDF]

  115. William Lovas and Frank Pfenning. A bidirectional refinement type system for LF. In B. Pientka and C. Schürmann, editors, Proceedings of the Second International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 113-128, Bremen, Germany, July 2007. Electronic Notes in Theoretical Computer Science (ENTCS), vol 196. [PDF]

  116. M. Berna, B. Lisien, B. Sellner, G. Gordon, F. Pfenning, , and S. Thrun. A learning algorithm for localizing people based on wireless signal strength that uses labeled and unlabeled data. In Proceedings of the 18th International Joint Conference on Artificial Intelligence (IJCAI'03), Acapulco, Mexico, August 2003. Poster. [PDF]

  117. Aleksandar Nanevski, Brigitte Pientka, and Frank Pfenning. A modal foundation for meta-variables. In Proceedings of the Second Workshop on Mechanized Reasoning about Languages with Variable Binding (MERLIN'03), Uppsala, Sweden, August 2003. ACM SIGPLAN.

  118. Bor-Yuh Evan Chang, Karl Crary, Margaret DeLap, Robert Harper, Jason Liszka, Tom Murphy VII, and Frank Pfenning. Trustless grid computing in ConCert. In M. Parashar, editor, Proceedings of the 3rd International Workshop on Grid Computing (GRID'02), pages 112-125, Baltimore, Maryland, November 2002. Springer-Verlag LNCS 2536. [PDF]

  119. Andreas Abel, Bor-Yuh Evan Chang, and Frank Pfenning. Human-readable, machine-verifiable proofs for teaching constructive logic. In Proceedings of the Workshop on Proof Transformations, Proof Presentations and Complexity of Proofs (PTP'01), Siena, Italy, June 2001. [PDF]

  120. Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In Joëlle Despeyroux, editor, 2nd Workshop on Logical Frameworks and Meta-languages (LFM'00), Santa Barbara, California, June 2000. Proceedings available as INRIA Technical Report. [PDF]

  121. Brigitte Pientka and Frank Pfenning. Termination and reduction checking in the logical framework. In Carsten Schürmann, editor, Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000. [PDF]

  122. Mark Plesko and Frank Pfenning. A formalization of the proof-carrying code architecture in a linear logical framework. In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, July 1999. [PDF]

  123. Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. A compilation manager for Standard ML of New Jersey. In Didier Rémy, editor, Record of the 1994 ACM SIGPLAN Workshop on ML and it Applications, pages 136-147, Orlando, Florida, June 1994. INRIA Technical Report 2265. Available as Technical Report CMU-CS-94-116.

  124. Frank Pfenning. Elf: A meta-language for deductive systems. In A. Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, pages 811-815, Nancy, France, June 1994. Springer-Verlag LNAI 814. System abstract. [PDF]

  125. Peter B. Andrews, Matthew Bishop, Sunil Issar, Dan Nesmith, Frank Pfenning, and Hongwei Xi. TPS: An interactive and automatic tool for proving theorems of type theory. In Jeffrey J. Joyce and Carl-Johan H. Seger, editors, Proceedings of the 6th International Workshop on Higher Order Logic Theorem Proving and Its Applications, pages 366-370, Vancouver, B.C., Canada, August 1993. Springer-Verlag LNCS 780.

  126. Frank Pfenning. Refinement types for logical frameworks. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, pages 285-299, Nijmegen, The Netherlands, May 1993. [PDF]

  127. Spiro Michaylov and Frank Pfenning. Higher-order logic programming as constraint logic programming. In Position Papers for the First Workshop on Principles and Practice of Constraint Programming, pages 221-229, Newport, Rhode Island, April 1993. Brown University. [PDF]

  128. Spiro Michaylov and Frank Pfenning. An empirical study of the runtime behavior of higher-order logic programs. In D. Miller, editor, Proceedings of the Workshop on the lambda Prolog Programming Language, pages 257-271, Philadelphia, Pennsylvania, July 1992. University of Pennsylvania. Available as Technical Report MS-CIS-92-86. [PDF]

  129. Peter B. Andrews, Sunil Issar, Dan Nesmith, and Frank Pfenning. The TPS theorem proving system. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 641-642, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. System abstract. [PDF]

  130. Frank Pfenning. Single axioms in the implicational propositional calculus. In Ewing Lusk and Ross Overbeek, editors, Proceedings of the 9th International Conference on Automated Deduction, pages 710-713, Argonne, Illinois, May 1988. Springer-Verlag LNCS 310. Problem set. [PDF]

    Technical Reports

  131. Deepak Garg, Frank Pfenning, Denis Serenyi, and Brian Witten. A logical representation of common rule for controlling access to classified information. Technical Report CMU-CS-09-139, Carnegie Mellon University, June 2009. [PDF]

  132. Henry DeYoung, Deepak Garg, and Frank Pfenning. An authorization logic with explicit time. Technical Report CMU-CS-07-166, Carnegie Mellon University, Department of Computer Science, December 2007. Revised February 2008. [PDF]

  133. Ruy Ley-Wild and Frank Pfenning. Avoiding causal dependencies via proof irrelevance in a concurrent logical framework. Technical Report CMU-CS-07-107, Carnegie Mellon University, February 2007. In preparation. [PDF]

  134. Boy-Yuh Evan Chang, Kaustuv Chaudhuri, and Frank Pfenning. A judgmental analysis of linear logic. Technical Report CMU-CS-03-131R, Carnegie Mellon University, Department of Computer Science, December 2003. [PDF]

  135. Iliano Cervesato, Frank Pfenning, David Walker, and Kevin Watkins. A concurrent logical framework II: Examples and applications. Technical Report CMU-CS-02-102, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. [PDF]

  136. Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101, Department of Computer Science, Carnegie Mellon University, 2002. Revised May 2003. [PDF]

  137. Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Unification via explicit substitutions: The case of higher-order patterns. Rapport de Recherche 3591, INRIA, December 1998. Preliminary version appeared at JICSLP'96.

  138. Jeff Polakow and Frank Pfenning. Ordered linear logic programming. Technical Report CMU-CS-98-183, Department of Computer Science, Carnegie Mellon University, December 1998. [PDF]

  139. Robert Harper, Peter Lee, and Frank Pfenning. The Fox project: Advanced language technology for extensible systems. Technical Report CMU-CS-98-107, Department of Computer Science, Carnegie Mellon University, January 1998. [PDF]

  140. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, Department of Computer Science, Carnegie Mellon University, April 1997. [PDF]

  141. Olivier Danvy and Frank Pfenning. The occurrence of continuation parameters in CPS terms. Technical Report CMU-CS-95-121, Department of Computer Science, Carnegie Mellon University, February 1995. [PDF]

  142. Frank Pfenning. Structural cut elimination in linear logic. Technical Report CMU-CS-94-222, Department of Computer Science, Carnegie Mellon University, December 1994. [PDF]

  143. Robert Harper, Peter Lee, and Frank Pfenning. Foundations of programming: Aspects of research in Ergo. In Computer Science Research Review 1988/1989, pages 29-37. School of Computer Science, Carnegie Mellon University, 1990.

  144. Peter Lee, Mark Leone, Spiro Michaylov, and Frank Pfenning. Towards a practical programming language based on the polymorphic lambda calculus. Ergo Report 89-085, School of Computer Science, Carnegie Mellon University, November 1989. [PDF]

  145. Scott Dietzen and Frank Pfenning. Explanation-based learning in logic programming. Ergo Report 89-086, Carnegie Mellon University, November 1989.

  146. Peter Lee, Frank Pfenning, John Reynolds, Gene Rollins, and Dana Scott. Research on semantically based program-design environments: The Ergo Project in 1988. Technical Report CMU-CS-88-118, Carnegie Mellon University, March 1988. [PDF]

  147. Conal Elliott and Frank Pfenning. A family of program derivations for higher-order unification. Ergo Report 87-045, Carnegie Mellon University, November 1987. [PDF]

    Other Publications

  148. Frank Pfenning. Possession as linear knowledge. In B.Farwer, editor, Proceedings of the 3rd International Workshop on Logics, Agents, and Mobility (LAM 2010), Edinburgh, Scotland, July 2010. Abstract of invited talk. To appear.

  149. Frank Pfenning. The practice and promise of substructural frameworks. In K.Crary and M.Miculan, editors, Proceedings of 5th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2010), Edinburgh, Scotland, July 2010. Abstract of invited talk. To appear.

  150. Jason C. Reed and Frank Pfenning. Focus-preserving embeddings of substructural logics in intuitionistic logic. Unpublished Manuscript, January 2010. [PDF]

  151. Lujo Bauer, Frank Pfenning, and Michael K. Reiter. Distributed system security via logical frameworks. In Information Security Research: New Methods for Protecting Against Cyber Threads, pages 108-115. Department of Defense, Wiley Publishing, 2007.

  152. Frank Pfenning. Subtyping and intersection types revisited. In R. Hinze and N. Ramsey, editors, Proceedings of the 12th International Symposium on Functional Programming (ICFP 2007), page 219, Freiburg, Germany, October 2007. ACM Press. Abstract of invited talk.

  153. Frank Pfenning. On a logical foundation for explicit substitutions. In S. Ronchi Della Rocca, editor, Proceedings of the 8th International Conference on Typed Lambda Calculi and Applications (TLCA 2007), page 1, Paris, France, June 2007. Springer LNCS 4583. Abstract of TLCA/RTA joint invited talk.

  154. Frank Pfenning. Towards a type theory of contexts. In Proceedings of the 3rd Workshop on Mechanized Reasoning About Languages with Variable Binding (MERLIN'05), page 1, Tallinn, Estonia, September 2005. ACM Press. Abstract for invited talk.

  155. Frank Pfenning. Review of ``Benjamin C. Pierce: Types and programming languages, The MIT Proess, Cambridge, Massachusetts, 2002''. Bulletin of Symbolic Logic, 10:213-214, 2004. [PDF]

  156. Frank Pfenning. Substructural operational semantics and linear destination-passing style. In W.-N. Chin, editor, Proceedings of the 2nd Asian Symposium on Programming Languages and Systems (APLAS'04), page 196, Taipei, Taiwan, November 2004. Springer-Verlag LNCS 3302. Abstract of invited talk. [PDF]

  157. Kaustuv Chaudhuri and Frank Pfenning. Resource management for the inverse method in linear logic. Draft manuscript, January 2003. [PDF]

  158. Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Modules matter most. Position paper presented at the NSF Workshop on New Visions for Software Design and Productivity, December 2001. Nashville, Tennessee. [PDF]

  159. Frank Pfenning. Logical frameworks at CMU. ALP Newsletter, 14(2), May 2001. Available electronically

  160. Frank Pfenning. Reasoning about staged computation. In W. Taha, editor, Proceedings of the International Workshop on Semantics, Applications, and Implementation of Program Generation (SAIG 2000), pages 5-6, Montreal, Canada, September 2000. Springer-Verlag LNCS 1924. Abstract of invited talk. Available electronically

  161. Frank Pfenning. On the logical foundations of staged computation. In Julia Lawall, editor, Proceedings of the Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM'00), page 33, Boston, Massachusetts, January 2000. ACM Press. Abstract of invited talk. Available electronically

  162. Frank Pfenning. Logical and meta-logical frameworks. In G. Nadathur, editor, Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP'99), page 206, Paris, France, September 1999. Springer-Verlag LNCS 1702. Abstract of invited talk.

  163. Frank Pfenning. Reasoning about deductions in linear logic. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the 15th International Conference on Automated Deduction (CADE-15), pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Abstract for invited talk. [PDF]

  164. Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173, Carnegie Mellon University.

  165. Frank Pfenning. The practice of logical frameworks. In Hélène Kirchner, editor, Proceedings of the Colloquium on Trees in Algebra and Programming, pages 119-134, Linköping, Sweden, April 1996. Springer-Verlag LNCS 1059. Invited talk. [PDF]

  166. Frank Pfenning. Logical frameworks. Home page and bibliography on the World-Wide Web, October 1994.

  167. Frank Pfenning. Types in logic programming. In David H.D. Warren and Peter Szeredi, editors, Proceedings of the Seventh International Conference on Logic Programming. MIT Press, June 1990. Abstract of advanced tutorial. [PDF]

  168. Amy Felty, Elsa Gunter, Dale Miller, and Frank Pfenning. Tutorial on lambda Prolog. In M.E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, page 682, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. Abstract. [PDF]

  169. Frank Pfenning. Review of ``Jean H. Gallier: Logic for Computer Science, Harper & Row, New York 1986''. Journal of Symbolic Logic, 54(1):288-289, March 1989.

  170. Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, January 1987. [PDF]

[ Home | Contact | Research | Publications | CV | Students ]
[ Projects | Courses | Conferences | Organizations | Journals ]
[ Logical Frameworks | Pittsburgh Squash Racquets Assocation ]

Frank Pfenning