Bibliography on LF and Elf

This is a bibliography on the LF logical framework, the logic programming language Elf which is based on LF, and the Twelf meta-logical framework (which includes an implementation of Elf). It is a selection of papers from a more general bibliography on logical frameworks. Papers with known URLs in the World-Wide Web have been annotated with their location and can be previewed or retrieved directly. Corrections, additions, and new URL's for papers and implementations are welcome.

Some pointers to basic references:

Last Updated: Tue Aug 3 1999
Compiled by Frank Pfenning

fp@cs.cmu.edu

  1. Penny Anderson. Program Derivation by Proof Transformation. PhD thesis, Carnegie Mellon University, October 1993. Available as Technical Report CMU-CS-93-206. Available electronically.

  2. Penny Anderson. Program extraction in a logical framework setting. In Frank Pfenning, editor, Proceedings of the 5th International Conference on Logic Programming and Automated Reasoning, pages 144-158, Kiev, Ukraine, July 1994. Springer-Verlag LNAI 822.

  3. Penny Anderson. Representing proof transformations for program optimization. In Proceedings of the 12th International Conference on Automated Deduction, pages 575-589, Nancy, France, June 1994. Springer-Verlag LNAI 814. Available electronically.

  4. Andrew W. Appel and Edward W. Felten. Proof-carrying authentication. In G. Tsudik, editor, Proceedings of the 6th Conference on Computer and Communications Security, Singapore, November 1999. ACM Press. To appear.

  5. Andrew W. Appel and Amy P. Felty. Lightweight lemmas in lambda prolog. In Danny De Schreye, editor, Proceedings of the International Conference on Logic Programming (ICLP'99), Las Cruces, New Mexico, December 1999. MIT Press. To appear.

  6. Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. Submitted, July 1999.

  7. David Aspinall and Adriana Compagnoni. Subtyping dependent types. In E. Clarke, editor, Proceedings of the 11th Annual Symposium on Logic in Computer Science, pages 86-97, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press.

  8. Arnon Avron, Furio A. Honsell, Ian A. Mason, and Robert Pollack. Using typed lambda calculus to implement formal systems on a machine. Journal of Automated Reasoning, 9(3):309-354, 1992. A preliminary version appeared as University of Edinburgh Report ECS-LFCS-87-31.

  9. Jason J. Brown. Presentations of Unification in a Logical Framework. PhD thesis, University of Oxford, January 1996.

  10. Rod Burstall and Furio Honsell. Operational semantics in a natural deduction setting. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 185-214. Cambridge University Press, 1991.

  11. Iliano Cervesato. A Linear Logical Framework. PhD thesis, Dipartimento di Informatica, Università di Torino, February 1996.

  12. Iliano Cervesato. Proof-theoretic foundation of compilation in logic programming languages. In J. Jaffar, editor, Proceedings of the 1998 Joint International Conference and Symposium on Logic Programming (JICSLP'98), pages 115-129, Manchester, UK, June 1998. MIT Press. Available in PostScript format.

  13. Iliano Cervesato, Joshua S. Hodas, and Frank Pfenning. Efficient resource management for linear logic proof search. Theoretical Computer Science, 1997. To appear in a special issue on Proof Search in Type-Theoretic Languages, D. Galmiche, editor. Available in PostScript format.

  14. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In D. Galmiche, editor, Informal Proceedings of the Workshop on Proof Search in Type-Theoretic Language, New Brunswick, New Jersey, July 1996. Available in PostScript format.

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

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

  17. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, Department of Computer Science, Carnegie Mellon University, April 1997. Available in PostScript format.

  18. Iliano Cervesato and Frank Pfenning. A linear logical framework. Information and Computation, 1998. To appear in a special issue with invited papers from LICS'96, E. Clarke, editor. Available in PostScript format.

  19. Thierry Coquand. An algorithm for testing conversion in type theory. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255-279. Cambridge University Press, 1991.

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

  21. Gilles Dowek. The undecidability of typability in the lambda-pi-calculus. In M. Bezem and J.F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 139-145, Utrecht, The Netherlands, March 1993. Springer-Verlag LNCS 664.

  22. Gilles Dowek, Gérard Huet, and Benjamin Werner. On the definition of the eta-long normal form in type systems of the cube. In Herman Geuvers, editor, Informal Proceedings of the Workshop on Types for Proofs and Programs, Nijmegen, The Netherlands, May 1993. Available in PostScript format.

  23. Conal Elliott. Higher-order unification with dependent types. In N. Dershowitz, editor, Rewriting Techniques and Applications, pages 121-136, Chapel Hill, North Carolina, April 1989. Springer-Verlag LNCS 355. Available in PostScript format.

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

  25. Conal M. Elliott. Extensions and Applications of Higher-Order Unification. PhD thesis, School of Computer Science, Carnegie Mellon University, May 1990. Available as Technical Report CMU-CS-90-134. Available in DVI and PostScript formats.

  26. Amy Felty. Encoding dependent types in an intuitionistic logic. In Gérard Huet and Gordon D. Plotkin, editors, Logical Frameworks, pages 214-251. Cambridge University Press, 1991. Available in PostScript format.

  27. Amy Felty and Dale Miller. Encoding a dependent-type lambda-calculus in a logic programming language. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 221-235, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. Available in PostScript format.

  28. Philippa Gardner. Representing Logics in Type Theory. PhD thesis, University of Edinburgh, July 1992. Available as Technical Report CST-93-92.

  29. Philippa Gardner. A new type theory for representing logics. In Andrei Voronkov, editor, Proceedings of the 4th International Conference on Logic Programming and Automated Reasoning (LPAR'93), pages 146-157, St. Petersburg, Russia, July 1993. Springer-Verlag LNAI 698.

  30. Wolfgang Gehrke. Problems in rewriting applied to categorical concepts by the example of a computational comonad. Technical Report CMU-CS-94-207, Carnegie Mellon University, Pittsburgh, Pennsylvania, October 1994. Available in DVI format.

  31. Wolfgang Gehrke. Proof of the decidability of the uniform word problem for monads assisted by Elf. Technical Report 94-66, RISC, Linz, Austria, August 1994. Available in DVI format.

  32. Wolfgang Gehrke. Decidability Results for Categorical Notions Related to Monads by Rewriting Techniques. PhD thesis, Research Institute for Symbolic Computation, Linz, Austria, May 1995. Available as RISC Report Number 95-30. Available in PostScript format.

  33. Wolfgang Gehrke. Problems in rewriting applied to categorical concepts by the example of a computational comonad. In Jieh Hsiang, editor, Proceedings of the Sixth International Conference on Rewriting Techniques and Applications, pages 210-224, Kaiserslautern, Germany, April 1995. Springer-Verlag LNCS 914. Available in PostScript format.

  34. Herman Geuvers. The Church-Rosser property for beta-eta-reduction in typed lambda-calculi. In A. Scedrov, editor, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 453-460, Santa Cruz, California, June 1992.

  35. Healfdene Goguen. Soundness of the logical framework for its typed operational semantics. In Jean-Yves Girard, editor, Proceedings of the 4th International Conference on Typed Lambda Calculi and Applications (TLCA'99), pages 177-197, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581.

  36. John Hannan. Searching for semantics. In D. Schmidt, editor, Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics Based Program Manipulation, pages 1-12, Copenhagen, Denmark, June 1993. Available in DVI format.

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

  38. Robert Harper. An equational formulation of LF. Technical Report ECS-LFCS-88-67, University of Edinburgh, 1988.

  39. Robert Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990. Available in DVI format.

  40. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. In Symposium on Logic in Computer Science, pages 194-204. IEEE Computer Society Press, June 1987.

  41. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the Association for Computing Machinery, 40(1):143-184, January 1993. Available in DVI format.

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

  43. Robert Harper, Donald Sannella, and Andrzej Tarlecki. Logic representation. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poigneé, editors, Proceedings of the Workshop on Category Theory and Computer Science, pages 250-272, Manchester, UK, September 1989. Springer-Verlag LNCS 389.

  44. Robert Harper, Donald Sannella, and Andrzej Tarlecki. Structure and representation in LF. In Fourth Annual Symposium on Logic in Computer Science, pages 226-237, Pacific Grove, California, June 1989. IEEE Computer Society Press.

  45. Robert Harper, Donald Sannella, and Andrzej Tarlecki. Structured presentations and logic representations. Annals of Pure and Applied Logic, 67:113-160, 1994. Available in PostScript format.

  46. John Hatcliff. Mechanically verifying the correctness of an offline partial evaluator. In M. Hermenegildo and S.D. Swierstra, editors, Proceedings of the 7th International Symposium on Programming Languages: Implementations, Logics and Programs, pages 279-298, Utrecht, The Netherlands, September 1995. Springer-Verlag LNCS 982. Available in PostScript format.

  47. Samin Ishtiaq and David Pym. A relevant analysis of natural deduction. Journal of Logic and Computation, 8(6):809-838, 1998.

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

  49. Chuck Liang. Substitutions for proofs and types as logic programming. In Didier Galmiche, editor, Informal Proceedings of the Workshop on Proof Search in Type-Theoretic Languages, pages 61-68, New Brunswick, New Jersey, July 1996.

  50. Ian A. Mason. Hoare's logic in the LF. Technical Report ECS-LFCS-87-32, Laboratory for Foundations of Computer Science, University of Edinburgh, June 1987.

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

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

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

  54. Marino Miculan. The expressive power of structural operational semantics with explicit assumptions. In Henk Barendregt and Tobias Nipkow, editors, Types for Proofs and Programs, pages 263-290. Springer-Verlag LNCS 806, 1994.

  55. Dale Miller, Gordon Plotkin, and David Pym. A relevant analysis of natural deduction. Talk given at the Workshop on Logical Frameworks, Båstad, Sweden, May 1992.

  56. George C. Necula. Proof-carrying code. In Neil D. Jones, editor, Conference Record of the 24th Symposium on Principles of Programming Languages (POPL'97), pages 106-119, Paris, France, January 1997. ACM Press.

  57. George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, October 1998. Available as Technical Report CMU-CS-98-154.

  58. George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of the Second Symposium on Operating System Design and Implementation (OSDI'96), pages 229-243, Seattle, Washington, October 1996.

  59. George C. Necula and Peter Lee. The design and implementation of a certifying compiler. In Keith D. Cooper, editor, Proceedings of the Conference on Programming Language Design and Implementation (PLDI'98), pages 333-344, Montreal, Canada, June 1998. ACM Press.

  60. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. In Proceedings of the 13th Annual Symposium on Logic in Computer Science (LICS'98), pages 93-104, Indianapolis, Indiana, June 1998. IEEE Computer Society Press.

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

  62. 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 DVI and PostScript formats.

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

  64. Frank Pfenning. Computation and deduction. Unpublished lecture notes, 277 pp. Revised May 1994, April 1996, May 1992.

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

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

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

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

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

  70. Frank Pfenning. A structural proof of cut elimination and its representation in a logical framework. Technical Report CMU-CS-94-218, Department of Computer Science, Carnegie Mellon University, November 1994. Available in DVI and PostScript formats.

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

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

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

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

  75. Frank Pfenning. Computation and Deduction. Cambridge University Press, 2000. In preparation. Draft from April 1997 available electronically. Available in PostScript format.

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

  77. Frank Pfenning and Carsten Schürmann. Algorithms for equality and unification in the presence of notational definitions. In D. Galmiche, editor, Proceedings of the CADE Workshop on Proof Search in Type-Theoretic Languages. Electronic Notes in Theoretical Computer Science, July 1998. Available in PostScript format.

  78. 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, 1998. To appear. Available in PostScript format.

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

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

  81. Luís Pinto and Roy Dyckhoff. Sequent calculi for the normal terms of the lambda-pi- and lambda-pi-sigma-calculi. In D. Galmiche, editor, Proceedings of the Workshop on Proof Search in Type-Theoretic Languages, volume 17 of Electronic Notes in Theoretical Computer Science, Lindau, Germany, July 1998. Elsevier Science. Available electronically.

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

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

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

  85. D. J. Pym. A note on representation and semantics in logical frameworks. In Didier Galmiche, editor, Informal Proceedings of the Workshop on Proof Search in Type-Theoretic Languages, pages 101-108, New Brunswick, New Jersey, July 1996.

  86. David Pym. Proofs, Search and Computation in General Logic. PhD thesis, University of Edinburgh, 1990. Available as CST-69-90, also published as ECS-LFCS-90-125.

  87. David Pym. A unification algorithm for the lambda-pi-calculus. International Journal of Foundations of Computer Science, 3(3):333-378, September 1992.

  88. David Pym and Lincoln Wallen. Investigations into proof-search in a system of first-order dependent function types. In M.E. Stickel, editor, Proceedings of the 10th International Conference on Automated Deduction, pages 236-250, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449.

  89. David Pym and Lincoln A. Wallen. Proof search in the lambda-pi-calculus. In Gérard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 309-340. Cambridge University Press, 1991.

  90. David Pym and Lincoln A. Wallen. Logic programming via proof-valued computations. In K. Broda, editor, Proceedings of the 4th UK Annual Conference on Logic Programming, London, March 1992. Springer-Verlag.

  91. David J. Pym. A note on the proof theory of the lambda-pi-calculus. Studia Logica, 54(2):199-230, 1995.

  92. Ekkehard Rohwedder. Verifying the meta-theory of deductive systems. Thesis Proposal, February 1994.

  93. Ekkehard Rohwedder. Verifying the Meta-Theory of Deductive Systems. PhD thesis, School of Computer Science, Carnegie Mellon University, 1996. Forthcoming.

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

  95. Anne Salvesen. The Church-Rosser theorem for LF with beta-eta-reduction. Unpublished notes to a talk given at the First Workshop on Logical Frameworks in Antibes, France, May 1990.

  96. Carsten Schürmann. A computational meta logic for the Horn fragment of LF. Master's thesis, Carnegie Mellon University, December 1995. Available as Technical Report CMU-CS-95-218.

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

  98. Aaron Stump and David L. Dill. Generating proofs from a decision procedure. In A. Pnueli and P. Traverso, editors, Proceedings of the FLoC Workshop on Run-Time Result Verification, Trento, Italy, July 1999.

  99. Roberto Virga. Higher-order superposition for dependent types. In Harald Ganzinger, editor, Proceedings of the 7th International Conference on Rewriting Techniques and Applications, pages 123-137, New Brunswick, New Jersey, July 1996. Springer-Verlag LNCS 1103. Extended version available as Technical Report CMU-CS-95-150, May 1995. Available in PostScript format.

  100. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, 1999. Forthcoming.