PETER LEE
Professor, Computer Science
www

My research interests are in the design and implementation of programming languages. This is an area that has become increasingly important and active in recent years, not only because of the obvious impact on software quality and security, but also because of the growing number of new domains for languages, such as web 2.0 applications.

Much of my recent research has focused on analysis and verification, especially concepts related to proof-carrying code and certifying compilers. This work is representative of my approach to research, which is to make practical applications based on sound theoretical foundations such as type theory, formal semantics, and applied logic. I have been particularly interested lately in the problem of how to expand the set of practical program properties that can be captured in a proof-carrying code system. My original work focused primarily on memory safety and simple type safety. But is it possible to incorporate higher-level concepts, such as correctness of list or tree data structures? What about freedom from memory leaks? Non-interference between threads? How might proof-carrying code be extended to provide information-flow guarantees?

To address some of these questions, I have been especially drawn to separation logic, which provides a basis for analysis and verification of pointer-based heap structures, and see how this might be incorporated into a certified code system. In another project, I have been investigating with several others how new logics might be used to extend a PCC system with the ability to keep track of who is allowed to make updates to system software. In both cases, the fundamental framework of PCC remains largely the same, and so much of the research involves (a) developing the logical foundations for capturing the properties of interest, and (b) devising (mostly automatic) proof methods so that proof-carrying code might be generated automatically.

I have also been drawn in recent years to think about the Claytronics Project. (See the entries for Seth Goldstein and Todd Mowry for more information about this project.) In the case of a Claytronics system, there is the very interesting question of how to program it. A Claytronics system might consist of thousands of computing nodes, each of which is moving and thus working in a constantly-changing network communications topology. It would be impossible to write sensible programs for each individual catom, and so languages and methods must devised that allow one to specify (hopefully declaratively) the global behavior of the system, and then to compile these specifications into the programs for the individual units. Some of the ideas developed thus far are based on logic-programming concepts, where achieving the desired global behavior is a matter of proof. While the current application for this language is a Claytronics system, ultimately this should have application to a wide variety of distributed programming problems.