Bibliography on the LF Logical Framework and the Elf Programming Language Compiled by Frank Pfenning Last updated January 15, 1993 This is a current list of Elf-related papers. The Elf tutorials, and most other Elf-related papers, and a suite of 16 examples from logic and the theory of programming languages are distributed via anonymous ftp. % ftp alonzo.tip.cs.cmu.edu Name: anonymous Password: (your e-mail address) ftp> cd /afs/cs/user/fp/public To retrieve the tutorial ftp> cd elf-papers ftp> get natsem91.dvi.Z ftp> bye % uncompress natsem91.dvi.Z will create the file natsem91.dvi which can be previewed or printed. Other papers archived in this directory are described in the file README. (alonzo.tip.cs.cmu.edu has internet address 128.2.209.194) References [Core Reference] [1] Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, To appear. Available as Technical Report CMU-CS-89-173, Carnegie Mellon University. A preliminary version appeared in Symposium on Logic in Computer Science, pages 194--204, June 1987. [Constraint Logic Programming] [2] 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. [3] Frank Pfenning. Logic programming in the LF logical framework. In Gerard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 149--181. Cambridge University Press, 1991. [4] 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. [Unification and Theorem Proving] [5] 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. [6] 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. [7] 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. [8] David Pym and Lincoln Wallen. Investigations into proof-search in a system of first-order dependent function types. In M.E. Stickel, editor, 10th International Conference on Automated Deduction, pages 236--250, Kaiserslautern, Germany, July 1990. Springer-Verlag LNCS 449. [9] 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. [Modularity] [10] 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. [11] Robert Harper, Donald Sannella, and Andrzej Tarlecki. Logic representation. In D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, and A. Poignee, editors, Proceedings of the Workshop on Category Theory and Computer Science, pages 250--272, Manchester, UK, September 1989. Springer-Verlag LNCS 389. [12] Robert Harper and Frank Pfenning. A module system for a programming language based on the LF logical framework. Technical Report CMU-CS-92-191, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992. [Extended Examples] [13] Arnon Avron, Furio A. Honsell, and Ian A. Mason. Using typed lambda calculus to implement formal systems on a machine. Technical Report ECS-LFCS-87-31, Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, June 1987. [14] Rod Burstall and Furio Honsell. Operational semantics in a natural deduction setting. In Gerard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 185--214. Cambridge University Press, 1991. [15] Ian A. Mason. Hoare's logic in the LF. Technical Report ECS-LFCS-87-32, Laboratory for Foundations of Computer Science, University of Edinburgh, Edinburgh, Scotland, June 1987. [16] Robert Harper. Systems of polymorphic type assignment in LF. Technical Report CMU-CS-90-144, Carnegie Mellon University, Pittsburgh, Pennsylvania, June 1990. [17] Spiro Michaylov and Frank Pfenning. Natural semantics and some of its meta-theory in Elf. In L.-H. Eriksson, L. Halln"as, 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. [Theory of and Variants of LF] [18] 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, May 1990. [19] Thierry Coquand. An algorithm for testing conversion in type theory. In Gerard Huet and Gordon Plotkin, editors, Logical Frameworks, pages 255--279. Cambridge University Press, 1991. [20] 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. IEEE Computer Society Press. [21] Philippa Gardner. Representing Logics in Type Theory. PhD thesis, University of Edinburgh, July 1992. Available as Technical Report CST-93-92. [22] Frank Pfenning. Intersection types for a logical framework. Submitted. Available as POP Report 92-006, School of Computer Science, Carnegie Mellon University, December 1992. [Metatheory in LF] [23] 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. [24] 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. IEEE Computer Society Press. [25] Frank Pfenning. A proof of the Church-Rosser theorem and its representation in a logical framework. Technical Report CMU-CS-92-186, Carnegie Mellon University, Pittsburgh, Pennsylvania, September 1992. [Implementation] [26] Frank Pfenning. An implementation of the Elf core language in Standard ML. Available via ftp over the Internet, September 1991. Send mail to elf-request@cs.cmu.edu for further information. [27] Spiro Michaylov and Frank Pfenning. An empirical study of the runtime behavior of higher-order logic programs. In Dale Miller, editor, Proceedings of the Workshop on the Lambda Prolog Programming Language, Philadelphia, Pennsylvania, July 1992. University of Pennsylvania. Also available as report POP-92-005, School of Computer Science, Carnegie Mellon University.