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
Proof-Carrying Code / Bibliography

This is a bibliography of research papers and reports related to Proof-Carrying Code from the Fox project at Carnegie Mellon University. The BibTeX source is available. 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. 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).

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

  3. 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 (Abstract, PDF).

  4. Karl Crary and Joseph C. Vanderwaart. An expressive, scalable type theory for certified code. Technical Report CMU-CS-01-113, School of Computer Science, Carnegie Mellon University, May 2001. Available electronically (Abstract, Postscript, PDF).

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

  6. George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, October 1998. Available as Technical Report CMU-CS-98-154. Available electronically (Abstract, Postscript, PDF).

  7. 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, Postscript).

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

  9. 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 (Abstract, Postscript).

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

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

  12. George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Giovanni Vigna, editor, Mobile Agents and Security, pages 61-91. Springer-Verlag LNCS 1419, August 1998. Available electronically.

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

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

[ 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/