Share on Facebook Tweet on Twitter Share on LinkedIn Share by email
Peter Lee

Peter Lee

Corporate Vice President,
Microsoft Research

As Corporate Vice President, Microsoft Research, Dr. Peter Lee oversees operations for an organization encompassing more than 1,000 scientists and engineers across multiple labs worldwide. Under Lee’s leadership, Microsoft Research conducts both basic and applied research across disciplines that include algorithms and theory; human-computer interaction; machine learning; multimedia and graphics; search; security; social computing; and systems, architecture, mobility and networking. Microsoft Research collaborates with the world's foremost researchers in academia, industry and government on initiatives to expand the state of the art across the breadth of computing and to help ensure the future of Microsoft's products.

Prior to joining Microsoft, Lee has held key positions in both government and academia. His most recent position was at the Defense Advanced Research Projects Agency (DARPA), where he founded and directed a major technology office that supported research in computing and related areas in the social and physical sciences. One of the highlights of his work at DARPA was the DARPA Network Challenge, which mobilized millions of people worldwide in a hunt for red weather balloons — a unique experiment in social media and open innovation that fundamentally altered the thinking throughout the Department of Defense on the power of social networks.

Before DARPA, Lee served as head of Carnegie Mellon University's nationally top-ranked computer science department. He also served as the university's vice provost for research. At CMU, he carried out research in software reliability, program analysis, security, and language design. He is well-known for his co-development of proof-carrying code techniques for enhanced software security, and has tackled problems as diverse as programming for large-scale modular robotics systems and shape analysis for C programs.

Lee is a Fellow of the Association for Computing Machinery and serves the research community at the national level, including policy contributions to the President’s Council of Advisors on Science and Technology and membership on both the National Research Council’s Computer Science and Telecommunications Board and the Advisory Council of the Computer and Information Science and Engineering Directorate of the National Science Foundation. He was the former chair of the Computing Research Association and has testified before both the US House Science and Technology Committee and the US Senate Commerce Committee.

Lee holds a Ph.D. in computer and communication sciences from the University of Michigan at Ann Arbor and bachelor's degrees in mathematics and computer sciences, also from the University of Michigan at Ann Arbor.

Affiliations and selected service activities

  • Member of the Advisory Council for the Computing and Information Science and Engineering Directorate of the National Science Foundation (NSF/CISE), 2012-present.
  • Co-chair of the NITRD Working Group for the President’s Council of Advisors on Science and Technology (PCAST). Conducting the congressionally mandated 2012 review of the federal Networking and Information Technology Research and Development (NITRD) program. (Final report publication is forthcoming.)
  • Testified before the US Senate Committee on Commerce, Science, and Transportation. 2012 hearing on Five Years of the America COMPETES Act: Progress, Challenges, and Next Steps.
  • Member of the National Research Council’s Computer Science and Telecommunications Board (CSTB) of the National Academies, 2007-2009 and 2011-present. Chair of the 2012 study resulting in publication of the book, Continuing Innovations in Information Technology.
  • Former member and Chair of the Board of the Computing Research Association (CRA), 2006-2008. Former Chair of the CRA Government Affairs Committee.
  • A founder of the CRA’s Computing Community Consortium (CCC), in 2008. Principal Investigator for the Computing Innovation Fellows Program (CIFellows) in 2009, providing over 100 postdoctoral fellowships to top new computer science PhDs.
  • Former Vice-Chair of the DARPA Information Science and Technology Board (ISAT), 2007-2008.
  • Testified before the US House a Committee on Science, Space, and Technology. Hearing on the Networking and Information Technology Research and Development Act of 2009.
  • Service on 25 conference program committees, including 6 conference and program committee chairmanships.

Awards and patents

  • 2006 SIGOPS Hall of Fame Award, for the most influential paper from OSDI ten or more years ago. Safe kernel extensions without run-time checking. George Necula and Peter Lee. November 2006.
  • ACM SIGPLAN Most Influential 1996 PLDI Paper. TIL: a type-directed optimizing compiler for ML. David Tarditi ,Greg Morrisett, Perry Cheng, Chris Stone, Robert Harper, and Peter Lee. June 2006.
  • Method and Apparatus for Enforcing Safety Properties of Computer Programs by Generating and Solving Constraints. Patent pending. Ajay Chander, Nayeem Islam, David Espinosa, Peter Lee, and George Necula.
  • Fellow of the Association for Computing Machinery. November 2004. Safe to Execute Verification of Software. US Patent 6,128,774, issued October 3, 2000, George Necula and Peter Lee.
  • 1997 Allen Newell Award for Research Excellence in Computer Science, for Proof-Carrying Code, awarded by the CMU School of Computer Science.
  • 1994 Herbert A. Simon Award for Teaching Excellence in Computer Science, awarded by the CMU School of Computer Science.
  • 1990 NSF Presidential Young Investigator, NSF CCR-9057567, $200,000. Matching funds from Bell Northern Research, $75,000.

Books

  • Peter Lee. Realistic Compiler Generation. The MIT Press Series in the Foundations of Computing, M. Garey and A. Meyer (Eds.), 1989.
  • Peter Lee (Editor). Topics in Advanced Language Implementation. The MIT Press, 1991.

Publications

  • Peter Lee and Uwe F. Pleban. On the use of LISP in implementing denotational semantics. Proceedings of the 1986 ACM Conference on LISP and Functional Programming, Cambridge, August 1986, 233-248.
  • Peter Lee and Uwe F. Pleban. A realistic compiler generator based on high-level semantics. Proceedings of the Fourteenth Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL’87), Munich, West Germany, January 1987, 284-295.
  • Uwe F. Pleban and Peter Lee. High-level semantics: an integrated approach to programming language semantics and the specification of implementations. The Third Workshop on the Mathematical Foundations of Programming Semantics (MFPS’87), New Orleans, April 1987, Proceedings appears in Lecture Notes in Computer Science, Vol. 298, M. Main (ed.), Springer-Verlag, June 1988.
  • Uwe F. Pleban and Peter Lee. An automatically generated, realistic compiler for an imperative language. Proceedings of the SIGPLAN '88 Conference on Programming Language Design and Implementation (PLDI’88), Atlanta, June 1988, 222-232.
  • Peter Lee, Frank Pfenning, Gene J. Rollins, and William S. Scherlis. The Ergo Support System: an integrated set of tools for prototyping integrated environments. Proceedings of the ACM SIGSOFT/SIGPLAN Software Engineering Symposium on Practical Software Development Environments, Peter Henderson (ed.), Boston, November 1988, 25-34.
  • Frank Pfenning and Peter Lee. LEAP: A Language with Eval and Polymorphism. TAPSOFT '89 Colloquium on Current Issues in Programming Languages, Barcelona, Spain, March 1989, Proceedings in Lecture Notes in Computer Science, Vols. 351 and 352, Springer-Verlag, 1989.
  • Philip J. Koopman, Jr. and Peter Lee. A fresh look at combinator graph reduction. Proceedings of the ACM SIGPLAN '89 Conference on Programming Language Design and Implementation (PLDI’89), Portland, Oregon, June 1989, 110-119.
  • Philip J. Koopman, Jr., Peter Lee, and Daniel P. Siewiorek. Cache performance of combinator graph reduction. Proceedings of the IEEE Computer Society 1990 International Conference on Computer Languages, New Orleans, March 1990, 39-48. A significantly revised and extended version appears as: Cache behavior of combinator graph reduction. ACM Transactions on Programming Languages and Systems, Vol. 14, No. 2, April 1992, 265-297.
  • Robert Nord and Peter Lee. Formal Manipulation of Modular Software Systems. ACM SIGSOFT International Workshop on Formal Methods in Software Development, Napa, California, May 1990. Peter Lee, May 2009 7 Refereed publications, continued:
  • Frank Pfenning and Peter Lee. Metacircularity in the polymorphic lambda calculus. Theoretical Computer Science, Vol. 89, 1991, 137-159.
  • Christopher Colby and Peter Lee. An implementation of parameterized partial evaluation. Actes JTASPEFL '91, Proceedings of the Conference on Static Analysis of Equational, Functional, and Logic Programs, Bordeaux, France, October 10-11, 1991, University of Bordeaux I, BIGRE 74, 82-89. An extended version appears as Technical Report CMU-CS-92-123, School of Computer Science, Carnegie Mellon University, Pittsburgh, March 1992.
  • David Tarditi, Peter Lee, and Anurag Acharya. No assembly required: Compiling Standard ML to C. ACM Letters on Programming Languages and Systems, Vol. 1, No. 2, June 1992, 161-177. (An earlier version is available as Carnegie Mellon School of Computer Science Technical Report CMU-CS-90-187, November 1990.)
  • David S. Touretzky and Peter Lee. Visualizing evaluation in applicative languages. Communications of the ACM, Vol. 35, No. 10, October 1992, 49-59. Also available as Technical Report CMU-CS-89-198-R, School of Computer Science, Carnegie Mellon University, Pittsburgh, November 1989.
  • Chris Okasaki, Peter Lee, and David Tarditi. Continuation-passing and graph reduction. Proceedings of the ACM SIGPLAN Workshop on Continuations (CW’92), June 21, 1992, San Francisco, 91-101. A significantly revised and extended version appears as: Call-by-need and continuation-passing style. Lisp and Symbolic Computation, Vol. 6, Nos. 3/4, November 1993, 57-82.
  • Edoardo Biagioni, Robert Harper, and Peter Lee. Signatures for a protocol stack: a systems application of Standard ML. Proceedings of the 1994 ACM Conference on Lisp and Functional Programming, Orlando, June 27-29. (An earlier version appears as Carnegie Mellon Computer Science Department Technical Report CMU-CS-93-170, September 1993.)
  • Robert Harper, Peter Lee, Frank Pfenning, and Eugene Rollins. Incremental recompilation for Standard ML of New Jersey. Proceedings of the Workshop on ML and Its Applications, Orlando, June 25-26, 1994. (An earlier version appears as Carnegie Mellon School of Computer Science Technical Report CMU-CSFOX-94-02, February 1994.)
  • Mark Leone and Peter Lee. Deferred compilation: the automation of run-time code generation. Proceedings of the Workshop on Partial Evaluation and Semantics-based Program Manipulation (PEPM'94), Orlando, June 25, 1994. (An earlier version appears as Carnegie Mellon School of Computer Science Technical Report CMU-CS-93-225, November 1993.)
  • Edoardo Biagioni, Robert Harper, and Peter Lee. Implementing Software Architectures in Standard ML. ICSE-17 Workshop on Research Issues in the Intersection of Software Engineering and Programming Languages, Seattle, April 24-25, 1995.
  • Christopher Colby and Peter Lee. Trace-based Program Analysis. Proceedings of the 1996 ACM SIGPLAN/SIGACT Symposium on Principles of Programming Languages (POPL’95), January 1996. Also available as Technical Report CMUCS-95-179 (Fox Memorandum CMU-CS-FOX-95-04), Department of Computer Science, Carnegie Mellon University, Pittsburgh, July 1995.
  • 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 Compiler for Standard ML. 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. Selected in 2006 as the Most Influential 1996 PLDI Paper.
  • 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. Winner of the 2006 SIGOPS Hall of Fame Award.
  • 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.
  • 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.
  • 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.
  • George C. Necula and Peter Lee. Efficient Representation and Validation of Proofs. Proceedings of the 13th 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. 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • 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.
  • Edoardo Biagioni, Robert Harper, and Peter Lee. A network protocol stack in Standard ML. Higher Order and Symbolic Computation, Vol.14, No.4, 2001.
  • 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.
  • 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.
  • Ajay Chander, David Espinosa, Peter Lee, and George C. Necula. Enforcing resource bounds via static verification of dynamic checks. 14th European Symposium on Programming (ESOP’05), held as part of ETAPS’05 (Edinburgh), Lecture Notes in Computer Science, April 2005, 311. Also available at http://www.springerlink.com/index/XT0WFRY9MK6BUPV5. Extended version invited for and submitted to a special issue of ACM Transactions on Programming Languages and Systems, To appear in 2006.
  • Ajay Chander, David Espinosa, Nayeem Islam, Peter Lee, and George Necula. JVer: a Java Verifier. 17th International Conference on Computer Aided Verification (CAV’05), July 2005.
  • Seth Copen Goldstein, Todd C. Mowry, Jason D. Campbell, Peter Lee, Padmanabhan Pillai, James F. Hoburg, Phillip B. Gibbons, Carlos Guestrin, James Kuffner, Brian Kirby, Benjamin D. Rister, Michael De Rosa, Stanislav Funiak, Burak Aksak, and Rahul Sukthankar. The Ensemble Principle. 13th Foresight Conference of Advanced Nanotechnogy, October 2005.
  • Stephen Magill, Aleksander Nanevsky, Edmund Clarke, and Peter Lee. Inferring Invariants in Separation Logic for Imperative List-processing Programs. The 3rd 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 Internatonal 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 Internatonal Conference on Robotics and Automation, (Orlando, FL), May 2006.
  • Michael De Rosa, Seth Goldstein, Peter Lee, Jason Campbell, Padmanabhan Pillai, and Todd Mowry. Distributed watchpoints: debugging large multi-robot systems. Proceedings of the 20067 IEEE Internatonal Conference on Robotics and Automation (ICRA’07).