Abstract: For most of the history of computing, programming languages have been viewed mainly as software engineering tools. Consequently, research in programming language design has focused on the construction of large software systems, with a special emphasis on supporting clear communication among humans. This research enterprise has been enormously successful, with some of the key advances reflected in the design and implementation of languages such as Java and ML. As important as these advances have been for the practice of software systems, we can see now that we are just barely scratching the surface. The key underlying technologies, such as type theory, formal semantics, and other applications of formal logic go beyond supporting the design of languages as software engineering tools, and make significant progress towards general mechanisms for free exchange of provably secure "plug-and-play" software components.

This talk will give an overview of some of the most recent research progress in programming languages, with an emphasis on verification and component technologies. It will start with some background on the current state of practice, leading to highlights of some of the most recent research directions aimed at supporting levels of security, composability, and performance that some envision will enable the construction of highly complex systems from multiple components and a new commerce the such components in an essentially "trustless" environment.

Bio: Peter Lee is a Professor and Associate Dean for Undergraduate Education in the School of Computer Science at Carnegie Mellon University. He joined the faculty in 1987, immediately after completing his Ph.D. in Computer and Communication Sciences at the University of Michigan. He is also the President of Cedilla Systems Incorporated, a Java technology startup company he co-founded in November of 1999. Lee is internationally respected for his research contributions in areas related to programming language design and implementation, and in particular to the application of language technology to problems related to building secure, reliable, and high-performance computer systems. He is perhaps best known for his work on the development of proof-carrying code, which promises to have many important applications in programming language design, compiler development, computer networking, and operating systems. A distinctive characteristic of Lee's work is that it makes use of theoretical results to solve practical problems in current practice.