Todd Millstein
University of California Los Angeles

Toward Programmer-Defined Effect Systems

Abstract:
One way that programmers manage the complexity of building and maintaining software systems is by  adhering to "programming disciplines" of various sorts.    For example, locking disciplines are used to prevent concurrency errors and ownership disciplines are used to enforce strong object encapsulation.    Over the past few years, colleagues and I have pursued an approach that allows programmers to specify desired disciplines, enforce them statically on programs, and validate these disciplines against intended run-time invariants.  For example, our Clarity framework supports user-defined type qualifiers for C and our JavaCOP framework supports "pluggable types" for Java.
 
After describing the overall motivation and structure of our approach, I will focus on some recent theoretical work toward allowing programmers to reason about computational effects of various kinds.    Type-and-effect systems are a natural solution and have been used to track memory, exceptions, locks, and many other kinds of effects.    We have defined a generic type-and-effect system, which is parameterized by a programmer-defined notion of effects along with rules for tracking these effects.    We have also architected a modular soundness proof for this type system, which depends on only a few natural properties of the programmer-defined rules.    We have formalized the type system and its metatheory in the Twelf proof assistant.
 
Bio:
Todd Millstein is an Assistant Professor in the Computer Science Department at the University of California, Los Angeles.  He designs language constructs that enhance the extensibility of classes in object-oriented languages while preserving modular reasoning.  Todd is also interested in techniques for static validation of software, including type systems and software model checking.  Todd received his Ph.D.  and M.S.  from the University of Washington and his A.B.  from Brown University, all in Computer Science.   He received an NSF CAREER award in 2006.
 
Host:  Peter Lee
Appointments:  Diana Hyde <dhyde@cmu.edu>

Co-sponsored by ISR Seminar Series



Wednesday, November 28, 2007
3:30 p.m.
Wean Hall 8220

Principles of Programming Seminars