Dependent type system for object-oriented programming languages

Typový systém s hodnotově-závislými typy pro objektově-orientované programovací jazyky

grant

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;

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.

Kolář Dušan, doc. Dr. Ing. (UIFS FIT VUT) , hlavní řešitel
Škarvada Libor, RNDr. (FI MUNI) , hlavní řešitel
Peterka Ondřej, Ing. (UIFS FIT VUT) , spoluřešitel
Ryšavý Ondřej, doc. Ing., Ph.D. (UIFS FIT VUT) , spoluřešitel