Dependent type system for object-oriented programming languages

Advanced type systems can provide more safety than type systems of programming
languages currently in use. Moreover, they can change the style of programming
discipline if used rigorously. The proposed project aims at basic research of
a new type system for object-oriented programming languages that allows to
guarantee safer programs, type check more language constructs and support the
correct-by-construction development and implementation methodology. The
contribution of the project comes with its approach. Shortly, we plan to emit
functional programming with dependent types into the object-oriented environment
and investigate the possible incidences. In particular, the dependent types in
subtyping imposed by class-based inheritance as the basic concept for reuse and
modularity, and the relation with traditional lambda-based theory are two main
topics that will be studied. An important part of the project is the development
of an experimental language featuring studied principles.