User-Defined Type Extensions

Type systems are a natural discipline for specifying and statically checking properties of programs. Researchers have shown how to extend types in traditional type systems to check many different classes of properties. For example, types have been used to statically ensure memory safety in the presence of manual memory management, lack of race conditions in the presence of multithreading, and proper (non)aliasing in the presence of pointers.

Of course, language designers cannot anticipate all the properties that programmers will want to specify and check. Language designers also cannot anticipate all of the practical ways in which types may be used in order to enforce a particular property. Therefore, it is desirable to provide a framework for user-defined type extensions, whereby programmers can easily augment a language's type system in order to ensure properties of interest.

The current focus of our efforts is JavaCOP, a framework for user-defined type annotations in Java. Programmers can employ annotations on Java classes, methods, fields, and variables using Java 1.5's metadata facility. JavaCOP enforces user-defined typing constraints for such annotations, which are written in a declarative and expressive rule language. In this way, programmers are able to check that their programs will operate correctly in restricted environments, adhere to strict programming rules, avoid null pointer errors or scoped memory exceptions, and meet style guidelines, while programming language researchers can easily experiment with novel type systems. JavaCOP can therefore be considered a framework for "pluggable type systems," whereby multiple type systems can be easily be supported in the same language.

Project Members

Chris Andreae (Victoria University of Wellington, New Zealand)
Brian Chin
Matt Esquivel
Dan Marino
Shane Markstrum
Todd Millstein
James Noble (Victoria University of Wellington, New Zealand)
Jens Palsberg

Publications

JavaCOP: Declarative Pluggable Types for Java    (TOPLAS 2010)
        Shane Markstrum, Daniel Marino, Matthew Esquivel, Todd Millstein, Chris Andreae, and James Noble

A Generic Type-and-Effect System    (TLDI 2009)
        Daniel Marino and Todd Millstein

Enforcing and Validating User-Defined Programming Disciplines   (PASTE 2007)
        Brian Chin, Daniel Marino, Shane Markstrum, and Todd Millstein

A Framework for Implementing Pluggable Type Systems    (OOPSLA 2006)
        Chris Andreae, James Noble, Shane Markstrum, and Todd Millstein

Inference of User-Defined Type Qualifiers and Qualifier Rules   (ESOP 2006)
        Brian Chin, Shane Markstrum, Todd Millstein, and Jens Palsberg

Semantic Type Qualifiers   (PLDI 2005)
        Brian Chin, Shane Markstrum, and Todd Millstein

Software

The JavaCOP release is here.