Dependent type system for object-oriented programming languages

Pokročilá typová kontrola dokáže zajistit vyšší míru správnosti programu než je
tomu běžné u současných programovacích jazyků. V některých případech použití
takového systému znamená změnu přístupu k programování obecně. Navrhovaný projekt
se zabývá základním výzkumem v oblasti typové kontroly pro objektově-orientovaný
programovací jazyk, který by umožnil odhalovat vyšší množství chyb, kontrolovat
složitější jazykové konstrukce a podporovat konstrukci korektních programů.
Přístup k řešení naznačuje předpokládaný přínos projektu. Jedná se zejména
o nalezení pozice hodnotově závislých typu v objektově-orientovaném typovaném
prostředí. Vztah závislých typů, podtypů a objektových typů a studium vlastností
takto definovaného systému včetně jeho vztahu k původní teorii jsou hlavní
teoretické části projektu. K projektu pak také patří konstrukce experimentálního
programovacího jazyka demonstrující studované vlastnosti.