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.
A Generic Type-and-Effect System
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
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