Publications by Peter Lee

Quick links to:

• Most frequently cited papers
• Most recent papers
• Unpublished manuscripts, popular articles, works-in-progress
• Other papers

This page is under construction. Check back later for a more complete list of publications.

Most recent papers:

• Ajay Chander, David Espinosa, Peter Lee, and George C. Necula. Enforcing resource bounds via static verification of dynamic checks. ACM Transactions on Programming Languages and Systems (TOPLAS), To appear.
• Stephen Magill, Aleksander Nanevsky, Edmund Clarke, and Peter Lee. Inferring invariants in separation logic for imperative list-processing programs. The 3^rd Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE’06), Charleston, SC, January 2006.
• Michael De Rosa, Seth Goldstein, Peter Lee, Jason Campbell, and Padmanabhan Pillai. Scalable shape sculpting via hole motion: Motion planning in lattice-constrained modular robots. Proceedings of the 2006 IEEE International Conference on Robotics and Automation (ICRA’06), Orlando, FL, May 2006.
• Seth Goldstein, Todd Mowry, Phillip Gibbons, Padmanabhan Pillai, Benjamin Rister, and Peter Lee. Ensembles of millions of microbots. Proceedings of the 2006 IEEE International Conference on Robotics and Automation (ICRA’06), Orlando, FL, May 2006.
• Insup Lee, George J. Pappas, Rance Cleaveland, John Hatcliff, Bruce Krogh, Peter Lee, and Lui Sha. High-confidence medical device software and systems. IEEE Computer Magazine, April 2006.

Most frequently cited papers:

• Christopher Colby, Peter Lee, George C. Necula, Fred Blau, Ken Cline, and Mark Plesko. A Certifying Compiler for Java. ACM SIGPLAN 2000 Conference on Programming Language Design and Implementation (PLDI’00), Vancouver, British Columbia, Canada, June 18-21, 2000.
• George Necula and Peter Lee. The design and implementation of a certifying compiler. ACM SIGPLAN'98 Conference on Programming Language Design and Implementation (PLDI’98), Montreal, June, 1998. Selected for the special issue: 20 Years of the ACM/SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection. ACM SIGPLAN Notices, Vol.39, No.4, April 2004.
• George Necula and Peter Lee. Safe kernel extensions without run-time checking. Proceedings of the Second Symposium on Operating System Design and Implementation (OSDI'96), Seattle, October, 1996, 229-243. Best Paper Award winner.
• Peter Lee and Mark Leone. Optimizing ML with Run-Time Code Generation. ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI’96), Philadelphia, May 1996. Selected for the special issue: 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection. ACM SIGPLAN Notices, Vol.39, No.4, April 2004. (An earlier version appears as Carnegie Mellon School of Computer Science Technical Report CMU-CS-95-205.)
• David Tarditi, Greg Morrisett, Perry Cheng, Christopher Stone, Robert Harper, and Peter Lee. The TIL/ML Compiler: Performance and safety through types. ACM SIGPLAN'96 Conference on Programming Language Design and Implementation (PLDI’96), Philadelphia, May 1996. Selected for the special issue: 20 Years of the ACM/SIGPLAN Conference on Programming Language Design and Implementation (1979-1999): A Selection. ACM SIGPLAN Notices, Vol.39, No.4, April 2004. (An earlier version appears as Carnegie Mellon School of Computer Science Technical Report CMU-CS-96-108, Fox Memorandum CMU-CS-FOX-96-01.)

Unpublished manuscripts, popular articles, works-in-progress:

Other selected papers:

• Christopher Colby, Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. Theoretical Computer Science (Special Issue on Dependable Computing), Vol.290, No.2, January 2003, 1175-1199.
• Andrew Bernard and Peter Lee. Temporal Logic for Proof-Carrying Code. CADE-18 Conference on Automated Deduction, volume 2392 of Lecture Notes in Computer Science, Copenhagen, Denmark, July 2002, 31-46.
• Edoardo Biagioni, Robert Harper, and Peter Lee. A network protocol stack in Standard ML. Higher Order and Symbolic Computation, Vol.14, No.4, 2001.
• Christopher Colby, Peter Lee, George C. Necula. A Proof-Carrying Code Architecture for Java. The 12th International Conference on Computer Aided Verification (CAV’00), Chicago, 15 July 2000.
• George C. Necula, Peter Lee. Proof Generation in the Touchstone Theorem Prover. Proceedings of the 17th International Conference on Automated Deduction (CADE’00), Pittsburgh, 13 June 2000.
• Karl Crary, Robert Harper, Peter Lee, and Frank Pfenning. Automated techniques for provably safe mobile code. 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.
• Perry Cheng, Robert Harper, and Peter Lee. Generational stack collection and profile-driven pretenuring. ACM SIGPLAN'98 Conference on Programming Language Design and Implementation (PLDI’98), Montreal, June, 1998.
• Philip Wickline, Peter Lee, and Frank Pfenning. Run-time code generation and Modal-ML. ACM SIGPLAN'98 Conference on Programming Language Design and Implementation (PLDI’98), Montreal, June, 1998.
• Andrew Bernard, Robert Harper, and Peter Lee. How generic is a generic back end? Using MLRISC as a back end for the TIL compiler. Types in Compilation ’98, Lecture Notes in Computer Science, No.1473, March 1998, 53-77.
• Mark Leone and Peter Lee. Dynamic specialization in the Fabius system. ACM Computing Surveys 1998 Symposium on Partial Evaluation (O. Danvy, R. Gluck, and P. Thiemann, Eds.), December, 1997.
• Philip Wickline, Peter Lee, Frank Pfenning, and Rowan Davies. Modal types as staging specifications for run-time code generation. ACM Computing Surveys 1998 Symposium on Partial Evaluation (O. Danvy, R. Gluck, and P. Thiemann, Eds.), December, 1997.
• George C. Necula and Peter Lee. Safe, Untrusted Agents Using Proof-Carrying Code. Mobile Agents and Security, Giovanni Vigna (Ed.), Lecture Notes in Computer Science, Vol. 1419, Springer-Verlag, Berlin, ISBN 3-540-64792-9, 1998.
• George C. Necula and Peter Lee. Efficient Representation and Validation of Proofs. Proceedings of the 13^th Annual Symposium on Logic in Computer Science (LICS’98), Indianapolis, June, 1998. (This is an abbreviated version of a 70-page technical report, CMU-CS-97-172, School of Computer Science, Carnegie Mellon University.)
• George C. Necula and Peter Lee. Research on Proof-Carrying Code for Untrusted-Code Security. Proceedings of the 1997 IEEE Symposium on Security and Privacy, Oakland, California, 1997.
• Edoardo Biagioni, Kenneth Cline, Peter Lee, Chris Okasaki, and Chris Stone. Safe-for-Space Threads in Standard ML. Second ACM SIGPLAN Workshop on Continuations (CW'97), Paris, January, 1997.
• P. Hartel, M. Feeley, M. Alt, L. Augustsson, P. Baumann, M. Beemster, E. Chailloux, C. H. Flood, W. Grieskamp, J. H. G. van Groningen, K. Hammond, B. Hausman, M. Y. Ivory, R. E. Jones, J. Kamperman, P. Lee, X. Leroy, R. D. Lins, S. Loosemore, N. Röjemo, M. Serrano, J.-P. Talpin, J. Thackray, S. Thomas, P. Walters, P. Weis, and P. Wentworth. Benchmarking Implementations of Functional languages with "Pseudoknot", a Float-Intensive Benchmark. Journal of Functional Programming, Vol.6, No.4, July 1996, 621-655.