Logical Frameworks at CMU

This is the home page for research on logical frameworks at Carnegie Mellon University.
Research on logical frameworks at CMU concentrates on the LF logical framework and its implementation in the Elf constraint logic programming language. The principal faculty members working on logical frameworks are Robert Harper and Frank Pfenning, both in the Department of Computer Science. The work is supported by NSF grant CCR-9303383.

For further information consult the home page on Elf or the more general home page on logical frameworks. These include a bibliography on LF and Elf and a bibliography on logical frameworks.

Faculty, Visitors, and Students

  • Iliano Cervesato, iliano@cs.cmu.edu
  • Robert Harper, robert.harper@cs.cmu.edu
  • Alberto Momigliano, am4e@andrew.cmu.edu
  • Frank Pfenning, fp@cs
  • Ekkehard Rohwedder, er@cs.cmu.edu
  • Carsten Schürmann, carsten@cs.cmu.edu
  • Roberto Virga, roberto.virga@cs.cmu.edu
  • Hao-Chi Wong, hcwong@cs.cmu.edu (1994-95)
  • Wolfgang Gehrke, wolfgang.gehrke@risc.uni-linz.ac.at (in 1994)
  • 1995/96 Reports and Publications

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

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

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

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

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

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

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

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

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

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

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

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

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

    Maintained by Frank Pfenning

    fp@cs