Teória programovania

Vývoj bezospornej matematickej teórie pre popis vnútornej štruktúry korektných programových systémov a pozorovanie ich vonkajšieho chovania.

Koordinátorka: prof. RNDr. Valerie Novitzká, PhD.

Formulovanie teoretických základov korektného programovania, ktoré považujeme za logické odvodzovanie nad teóriou typov.
Konštruovanie teórie typov pre základné, Churchove, polymorfické a závislé typy v pojmoch teórie kategórií a skúmanie ich vlastností.
Rozšírenie konečných sekvenčných a stromových automatov o typy tak, aby poskytovali mechanizmus pre typovú kontrolu a vyhodnocovanie termov teórie typov.
Definovanie logického systému ako funktora fibrácie nad teóriou typov a skúmanie jeho vlastností použitím toposov.
Lineárna logika ako zdrojovo-orientovaná logika pre popis dynamických systémov.
Interakčné kategórie ako štruktúry pre popis súbežných procesov.
Algebraická konštrukcia a koalgebraické pozorovanie v paradigme objektovo-orientovaného programovania
Skúmanie chovania systému pozorovaním zmien jeho vnútorných stavov a konštrukcia behaviorálnych modelov pre rozsiahle programové systémy.