Type System and Language Design

Good Type Systems are helpful to programmers who want to write correct and efficient code. Ideally, they also have nice properties that make it easy to implement and use them correctly, such as decidability. Lastly, many problems of a type system feature only show up when it is composed with others.

The work here is motivated by both an appreciation of the mathematical elegance of good definitions and the needs of other projects, in particular gradual typing and useful IDEs. It therefore largely focuses on problems in object-oriented languages.