Combining dependent types with object-oriented programming: a preliminary study

Dependently-typed programming languages allow constraints on the processing of data to be expressed through more expressive types than in standard languages. Although a number of dependently-typed programming languages currently exist, these languages generally follow a functional programming model. The combination of dependent types with the widely used object-oriented programming model has not yet been extensively studied. This project provides the basis for future study of this combination through the development of a type system combining key aspects of the Java language with the concepts of pure type systems. A prototype language implementation based on this new type system is used to evaluate the effectiveness of using more expressive types to improve the safety of typical object-oriented programming.