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.