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