Home
Contact Information
Publications
Researchers
Focus Areas
FoxNet
Typed Intermediate Languages
Proof-Carrying Code
Logical Frameworks
Staged Computation
Language Design
 
Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/
  

The Fox Project
Logical Frameworks / Bibliography

This is a bibliography of research papers and reports related to logical frameworks from the Fox project at Carnegie Mellon University. The BibTeX source is available. This is only indirectly related to Frank Pfenning's much more extensive 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 URLs for papers and implementations are welcome.

Last updated: Fri May 4 2001

  1. 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 International Workshop on Extensions of Logic Programming, pages 67-81, Leipzig, Germany, March 1996. Springer-Verlag LNAI 1050. Available electronically.

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

  3. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. Submitted for publication to the Journal of Symbolic Computation.

  4. Iliano Cervesato and Frank Pfenning. A linear logical framework. Submitted for publication to Information and Computation. Available electronically.

  5. 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, pages 41-50, New Brunswick, New Jersey, July 1996. Available electronically.

  6. Iliano Cervesato and Frank Pfenning. A linear logical framework. In E. Clarke, editor, Proceedings of the Symposium on Logic in Computer Science, pages 264-275, New Brunswick, New Jersey, July 1996. IEEE Computer Society Press. This work also appeared as Preprint 1834 of the Department of Mathematics of Technical University of Darmstadt, Germany. Available electronically (DVI, Postscript).

  7. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. Technical Report CMU-CS-97-160, School of Computer Science, Carnegie Mellon University, July 1997. Available electronically.

  8. Iliano Cervesato and Frank Pfenning. Linear higher-order pre-unification. In Glynn Winskel, editor, Proceedings of the Symposium on Logic in Computer Science, pages 422-433, Warsaw, Poland, June 1997. IEEE Computer Society Press. Available electronically (DVI, Postscript).

  9. Iliano Cervesato and Frank Pfenning. A linear spine calculus. Technical Report CMU-CS-97-125, School of Computer Science, Carnegie Mellon University, April 1997. Available electronically.

  10. Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. To appear in a special issue of Theoretical Computer Science on Dependable Computing. Available electronically (Abstract, Postscript, PDF).

  11. Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Mark Plesko, and Kenneth Cline. A certifying compiler for Java. In Proceedings of the Conference on Programming Language Design and Implementation, pages 95-107, Vancouver, Canada, June 2000. ACM Press. Available electronically.

  12. Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. In Proceedings of the DARPA Information Survivability Conference and Exposition, volume 1, pages 406-419, Hilton Head Island, South Carolina, January 2000. IEEE Computer Society Press. Available electronically.

  13. Robert Harper, Furio Honsell, and Gordon Plotkin. A framework for defining logics. Journal of the ACM, 40(1):143-184, January 1993. Available electronically (Postscript, PDF).

  14. 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, February 1998.

  15. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory (extended abstract). In Amy Felty, editor, Proceedings of the Workshop on Logical Frameworks and Meta-Languages, Paris, France, September 1999. Available electronically (Abstract, Postscript).

  16. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Technical Report CMU-CS-99-159, School of Computer Science, Carnegie Mellon University, September 1999. Available electronically (Abstract, Postscript, PDF).

  17. Robert Harper and Frank Pfenning. On equivalence and canonical forms in the LF type theory. Technical Report CMU-CS-00-148, School of Computer Science, Carnegie Mellon University, July 2000. Available electronically (Abstract, Postscript, PDF).

  18. George C. Necula. Proof-carrying code. In Neil D. Jones, editor, Proceedings of the Symposium on Principles of Programming Languages, pages 106-119, Paris, France, January 1997. ACM Press. Available electronically (Abstract, Postscript).

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

  20. George C. Necula and Peter Lee. Proof-carrying code. Technical Report CMU-CS-96-165, School of Computer Science, Carnegie Mellon University, September 1996. Available electronically (Abstract).

  21. George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of the Symposium on Operating System Design and Implementation, pages 229-243, Seattle, Washington, October 1996. Available electronically (Abstract, HTML, Postscript).

  22. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. Technical Report CMU-CS-97-172, School of Computer Science, Carnegie Mellon University, October 1997. Available electronically.

  23. 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, pages 333-344, Montreal, Canada, June 1998. ACM Press. Available electronically (Abstract, Postscript).

  24. George C. Necula and Peter Lee. Efficient representation and validation of logical proofs. In Vaughan Pratt, editor, Proceedings of the Symposium on Logic in Computer Science, pages 93-104, Indianapolis, Indiana, June 1998. IEEE Computer Society Press. Available electronically (Abstract, Postscript).

  25. George C. Necula and Peter Lee. Proof generation in the Touchstone theorem prover. In David McAllester, editor, Proceedings of the International Conference on Automated Deduction, pages 25-44, Pittsburgh, Pennsylvania, June 2000. Springer-Verlag LNAI 1831. Available electronically.

  26. Frank Pfenning. Logical frameworks. In press. Chapter 16 of Alan Robinson and Andrei Voronkov, editors, Handbook of Automated Reasoning, to be published by Elsevier Science and MIT Press.

  27. 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 electronically (DVI, Postscript).

  28. Frank Pfenning. Computation and deduction. Early draft of book to be published by Cambridge University Press, April 1997. Available electronically.

  29. Frank Pfenning. Reasoning about deductions in linear logic. In Claude Kirchner and Hélène Kirchner, editors, Proceedings of the International Conference on Automated Deduction, pages 1-2, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Abstract for invited talk. Available electronically.

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

  31. Frank Pfenning. Structural cut elimination I. intuitionistic and classical logic. Information and Computation, 157(1/2):84-141, March 2000. Available electronically.

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

  33. 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, Proceedings of the Workshop on Types for Proofs and Programs, pages 179-193, Kloster Irsee, Germany, March 1998. Springer-Verlag LNCS 1657. Available electronically.

  34. Frank Pfenning and Carsten Schürmann. Twelf User's Guide, 1.2 edition, September 1998. Available as Technical Report CMU-CS-98-173. Available electronically (HTML).

  35. Frank Pfenning and Carsten Schürmann. System description: Twelf - A meta-logical framework for deductive systems. In H. Ganzinger, editor, Proceedings of the International Conference on Automated Deduction, pages 202-206, Trento, Italy, July 1999. Springer-Verlag LNAI 1632. Available electronically.

  36. Brigitte Pientka and Frank Pfenning. Termination and reduction checking in the logical framework. In Carsten Schürmann, editor, Proceedings of the CADE Workshop on Automation of Proofs by Mathematical Induction, Pittsburgh, Pennsylvania, June 2000. Available electronically.

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

  38. Jeff Polakow and Frank Pfenning. Natural deduction for intuitionistic non-commutative linear logic. In J.-Y. Girard, editor, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 295-309, L'Aquila, Italy, April 1999. Springer-Verlag LNCS 1581. Available electronically.

  39. 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 Conference on Mathematical Foundations of Programming Semantics, New Orleans, Louisiana, April 1999. Electronic Notes in Theoretical Computer Science, Volume 20. Available electronically.

  40. Jeff Polakow and Frank Pfenning. Properties of terms in continuation-passing style in an ordered logical framework. In Joëlle Despeyroux, editor, Proceedings of the Workshop on Logical Frameworks and Meta-languages, Santa Barbara, California, June 2000. Available electronically.

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

  42. Carsten Schürmann. Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University, August 2000. Available as Technical Report CMU-CS-00-146. Available electronically.

  43. Carsten Schürmann. A meta logical framework based on realizability. In Joëlle Despeyroux, editor, Proceedings of the Workshop on Logical Frameworks and Meta-Languages, Santa Barbara, California, June 2000. Available electronically.

  44. 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 International Conference on Automated Deduction, pages 286-300, Lindau, Germany, July 1998. Springer-Verlag LNCS 1421. Available electronically.

  45. Roberto Virga. Higher-Order Rewriting with Dependent Types. PhD thesis, Department of Mathematical Sciences, Carnegie Mellon University, September 1999. Available as Technical Report CMU-CS-99-167. Available electronically (DVI, Postscript, PDF).

[ Home | Contact Information | Publications | Researchers ]
[ FoxNet | Typed Intermediate Languages | Proof-Carrying Code ]
[ Logical Frameworks | Staged Computation | Language Design ]

Fox_Project@cs.cmu.edu
http://www.cs.cmu.edu/~fox/