Bibliography of Proof-Carrying Code

[1]

Andrew W. Appel and Amy P. Felty. Lightweight lemmas in Lambda Prolog. In 16th International Conference on Logic Programming, pages 411--425. MIT Press, November 1999.

[2]

Andrew W. Appel and Amy P. Felty. A semantic model of types and machine instructions for proof-carrying code. In Conference Record of POPL '00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 243--253, January 2000.

[3]

Andrew W. Appel and Neophytos G. Michael. Machine instruction syntax and semantics in higher order logic. In 17th International Conference on Automated Deduction (CADE-17), Lecture Notes in Artificial Intelligence. Springer-Verlag, June 2000.

[4]

Christopher Colby, Peter Lee, and George C. Necula. A proof-carrying code architecture for Java. In Proceedings of the 12th International Conference on Computer Aided Verification (CAV00), Chicago, July 2000.

[5]

Christopher Colby, Peter Lee, George C. Necula, and Fred Blau. A certifying compiler for Java. In Proceedings of the ACM SIGPLAN'00 Conference on Programming Language Design and Implementation (PLDI), Vancouver, Canada, June 2000.

[6]

Karl Crary. A simple proof technique for certain parametricity results. In Proceedings of the Fourth International Conference on Functional Programming (ICFP '99), pages 82--89, Paris, France, September 1999.

[7]

Karl Crary and Greg Morrisett. Type structure for low-level programming languages. In 1999 International Colloquium on Automata, Languages, and Programming, 1999.

[8]

Karl Crary, David Walker, and Greg Morrisett. Typed memory management in a calculus of capabilities. In Conference Record of POPL '99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 262--275, January 1999.

[9]

Karl Crary and Stephanie Weirich. Flexible type analysis. In Proceedings of the Fourth International Conference on Functional Programming (ICFP '99), pages 233--248, Paris, France, September 1999.

[10]

Karl Crary and Stephanie Weirich. Resource bound certification. In Conference Record of POPL '00: The 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 184--198, January 2000.

[11]

Neal Glew. Type dispatch for named hierarchical types. In Proceedings of the Fourth International Conference on Functional Programming (ICFP '99), pages 172--182, Paris, France, September 1999.

[12]

Neal Glew and Greg Morrisett. Type-safe linking and modular assembly language. In Conference Record of POPL '99: The 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 250--261, January 1999.

[13]

Luke Hornof and Trevor Jim. Certifying compilation and run-time code generation. Higher-Order and Symbolic Computation, 12(4):337--375, December 1999. An earlier version appeared in Partial Evaluation and Semantics-Based Program Manipulation, 1999.

[14]

Dexter Kozen. Efficient code certification. Technical Report 98--1661, Cornell University, January 1998.

[15]

Greg Morrisett, Karl Crary, Neal Glew, Dan Grossman, Richard Samuels, Frederick Smith, David Walker, Stephanie Weirich, and Steve Zdancewic. TALx86: A realistic typed assembly language. In 1999 ACM SIGPLAN Workshop on Compiler Support for System Software, pages 25--35, Atlanta, GA, May 1999.

[16]

Greg Morrisett, Karl Crary, Neal Glew, and David Walker. Stack-based typed assembly language. In 1998 Workshop on Types in Compilation, Kyoto, Japan, March 1998.

[17]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. In Conference Record of POPL '98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 85--97, January 1998.

[18]

Greg Morrisett, David Walker, Karl Crary, and Neal Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528--569, May 1999.

[19]

George C. Necula. Proof-carrying code. In Conference Record of POPL '97: The 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 106--119, Paris, France, 15--17 January 1997.

[20]

George C. Necula. Compiling with Proofs. PhD thesis, Carnegie Mellon University, September 1998.

[21]

George C. Necula. Translation validation for an optimizing compiler. In Proceedings of the ACM SIGPLAN'00 Conference on Programming Language Design and Implementation (PLDI), Vancouver, Canada, June 2000.

[22]

George C. Necula and Peter Lee. Safe kernel extensions without run-time checking. In Proceedings of the Second Symposium on Operating Systems Design and Implementation, pages 229--243, Seattle, WA, October 1996.

[23]

George C. Necula and Peter Lee. Research on proof-carrying code for untrusted-code security. In Proceedings of the 1997 IEEE Symposium on Security and Privacy, Oakland, CA, 1997.

[24]

George C. Necula and Peter Lee. Research on proof-carrying code on mobile-code security. In Proceedings of the Workshop on Foundations of Mobile Code Security, Monterey, CA, 1997.

[25]

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

[26]

George C. Necula and Peter Lee. Efficient representation and validation of proofs. In Proceedings of the 13th Annual symposium on Logic in Computer Science, 1998.

[27]

George C. Necula and Peter Lee. Safe, untrusted agents using proof-carrying code. In Special Issue on Mobile Agent Security, number 1419 in Lecture Notes in Computer Science. Springer-Verlag, 1998.

[28]

George C. Necula and Peter Lee. Proof generation in the Touchstone theorem prover. In Proceedings of the 17th International Conference on Automated Deduction, Pittsburgh, June 2000.

[29]

Atsushi Ohori. A Curry-Howard isomorphism for compilation and program execution. In Proc. Typed Lambda Calculi and Applications, number 1581 in Lecture Notes in Computer Science, pages 258--179. Springer-Verlag, 1999.

[30]

Atsushi Ohori. The Logical Abstract Machine: a Curry-Howard isomorphism for machine code. In Proceedings of the Fuji International Symposium on Functional and Logic Programming, number 1722 in Lecture Notes in Computer Science, pages 300--318. Springer-Verlag, November 1999.

[31]

Frederick Smith, David Walker, and Greg Morrisett. Alias types. In European Symposium on Programming, Berlin, March 2000.

[32]

Hongwei Xi. Imperative programming with dependent types. In Proceedings of the 15th Symposium on Logic in Computer Science (LICS '00), Santa Barbara, June 2000.

[33]

Hongwei Xi and Robert Harper. A dependently typed assembly language. Technical Report OGI--CSE--99--008, Oregon Graduate Institute, July 1999.

[34]

Zhichen Xu, Barton P. Miller, and Thomas Reps. Safety checking of machine code. In Proceedings of the ACM SIGPLAN'00 Conference on Programming Language Design and Implementation (PLDI), Vancouver, Canada, June 2000.

This document was translated from L^AT_EX by H^EV^EA.