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.

Popis česky
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.

Klíčová slova

dependent types; formal reasoning; functional programming; lambda calculus; language constructs and features; object calculus; object orientation; program specification and verification; type theory;

Klíčová slova česky

hodnotově-závislé typy; formální odvozování; funkcionální programování; lambda kalkul; jazykové konstrukce; objektový kalkul; objektová-orientace; specifikace a ověřování programů; teorie typu;