Frank Pfenning's Bibliography

This is my bibliography sorted by publication type, in reverse chronological order. Links to PostScript files are given where available. My home page is more likely to be up to date, with recent papers and drafts in reverse chronological order.

  1. My home page
  2. Twelf home page
  3. Logical Frameworks home page

Last Updated Fri Aug 13 1999
Frank Pfenning

fp@cs

  1. Books
  2. Book Chapters
  3. Journal Papers - Published
  4. Journal Papers - Accepted
  5. Journal Papers - Submitted
  6. Refereed Conference and Workshop Papers
  7. Unrefereed Conference and Workshop Papers
  8. Technical Reports
  9. Other Publications

    Books

  1. Maurizio Gabrielli and Frank Pfenning, editors. Proceedings of the International Conference on Principles and Practice of Declarative Programming (PPDP'00), Ottawa, Canada, September 2000. Springer-Verlag LNCS. To appear.

  2. Frank Pfenning. Computation and deduction. Lecture notes, 312 pp. First version May 1992, April 1997. Cambridge University Press. In preparation for publication in Spring 2000.

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

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

    Book Chapters

  5. Frank Pfenning. Logical frameworks. In Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning. Elsevier Science Publishers, 1999. In preparation.

  6. 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. Springer-Verlag LNCS 1657, 1999. To appear. Available in PostScript format.

  7. 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.

  8. 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.

  9. 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. Available in PostScript format.

  10. 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

  11. 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. Available in PostScript format.

  12. 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.

  13. Paliath Narendran, Frank Pfenning, and Richard Statman. On the unification problem for Cartesian closed categories. Journal of Symbolic Logic, 62(2):636-647, 1997. Extended and revised version of [Narendran93].

  14. 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.

  15. Frank Pfenning. On the undecidability of partial polymorphic type reconstruction. Fundamenta Informaticae, 19(1,2):185-199, 1993. Available in DVI and PostScript formats.

  16. Scott Dietzen and Frank Pfenning. Higher-order and modal logic as a framework for explanation-based generalization. Machine Learning, 9:23-55, 1992. Extended and revised version of [Dietzen89ml].

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

  18. 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. Available in DVI format.

  19. Frank Pfenning. Program development through proof transformation. Contemporary Mathematics, 106:251-262, 1990.

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

    Journal Papers - Accepted

  21. Carsten Schürmann, Jöelle Despeyroux, and Frank Pfenning. Primitive recursion for higher-order abstract syntax. Theoretical Computer Science, 1999. To appear. Preliminary version available as Technical Report CMU-CS-96-172, December 1997. Extended and revised version of [Despeyroux97].

  22. Iliano Cervesato and Frank Pfenning. A linear logical framework. Information and Computation. To appear. Extended and revised version of [Cervesato96lics]. Available in PostScript format.

  23. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science. Extended and revised version of [Cervesato96elp]. Available in PostScript format.

  24. Frank Pfenning. Structural cut elimination I: Intuitionistic and classical logic. Information and Computation. Extended and revised version of [Pfenning95lics].

  25. Frank Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Journal of Automated Reasoning. To appear. A preliminary version is available as Carnegie Mellon Technical Report CMU-CS-92-186, September 1992. Available in DVI and PostScript formats.

    Journal Papers - Submitted

  26. Rowan Davies and Frank Pfenning. A modal analysis of staged computation. Submitted to JACM. Available as Technical Report CMU-CS-99-153, August 1999. Extended and revised version of [Davies96popl] Available in PostScript format.

  27. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. Submitted to JSC. Available as Technical Report CMU-CS-97-160, Department of Computer Science, Carnegie Mellon University, July 1997. Extended and revised version of [Cervesato97lics]. Available electronically.

    Refereed Conference and Workshop Papers

  28. 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, Paris, September 1999. To appear in Electronic Notes in Theoretical Computer Science. Available in PostScript format.

  29. 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), Las Cruces, New Mexico, November 1999. MIT Press. To appear. Available in PostScript format.

  30. 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. Available in PostScript format.

  31. 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. Available in PostScript format.

  32. 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, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20. Available in PostScript format.

  33. 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. Available electronically.

  34. 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. Available in PostScript format.

  35. 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. Available in PostScript format.

  36. 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. Available in PostScript format.

  37. 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. Available in DVI and PostScript formats.

  38. 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. Available in DVI and PostScript formats.

  39. 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. Available in DVI and PostScript formats.

  40. 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. Available in DVI and PostScript formats.

  41. 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. Available in PostScript format.

  42. 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. Available in DVI and PostScript formats.

  43. 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. Extended version available as Technical Report CMU-CS-95-145, Carnegie Mellon University, May 1995. Available in PostScript format.

  44. 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. Available in PostScript format.

  45. 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. Available in DVI and PostScript formats.

  46. 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. Available in DVI and PostScript formats.

  47. 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. Available in DVI and PostScript formats.

  48. 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. Available in DVI and PostScript formats.

  49. 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. Available in DVI and PostScript formats.

  50. 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.

  51. 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. Available in DVI and PostScript formats.

  52. 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. Available in DVI and PostScript formats.

  53. 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. Available in DVI and PostScript formats.

  54. 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.

  55. 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.

  56. 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.

  57. 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. Available in DVI and PostScript formats.

  58. 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.

  59. 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.

  60. 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.

  61. 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.

  62. 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.

  63. 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. Available in PostScript format.

  64. 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.

    Unrefereed Conference and Workshop Papers

  65. 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 Workshop on Run-Time Result Verification, Trento, Italy, July 1999. Available electronically.

  66. 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.

  67. 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. Available in DVI and PostScript formats.

  68. 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.

  69. 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. Available in DVI and PostScript formats.

  70. 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. Available in PostScript format.

  71. 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. Available in DVI and PostScript formats.

  72. 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.

  73. 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.

    Technical Reports

  74. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Submitted to the Workshop on Logical Frameworks and Meta-Languages, Paris, France, September 1999. Extended version to appear as Technical Report CMU-CS-99-159. Available in PostScript format.

  75. Jeff Polakow and Frank Pfenning. Ordered linear logic programming. Submitted to POPL'00. Available as Technical Report CMU-CS-98-183, Department of Computer Science, Carnegie Mellon University, December 1998. Available electronically.

  76. 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. Available electronically.

  77. 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. Available in PostScript format.

  78. Frank Pfenning. Structural cut elimination in linear logic. Technical Report CMU-CS-94-222, Department of Computer Science, Carnegie Mellon University, December 1994. Available in PostScript format.

  79. 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.

  80. 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.

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

  82. 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.

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

    Other Publications

  84. 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), Paris, France, September 1999. Springer-Verlag LNCS. Abstract of invited talk. To appear.

  85. 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. Available in PostScript format.

  86. 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. Available in DVI and PostScript formats.

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

  88. 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.

  89. 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.

  90. 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.

  91. Frank Pfenning. Proof Transformations in Higher-Order Logic. PhD thesis, Carnegie Mellon University, January 1987.