O projekte
Moderné prístupy a nástroje pre výučbu predmetov na univerzitnej úrovni v oblasti teoretickej informatiky, logiky, teórie typov a sémantiky, iniciatíva číslo: FBR-PDI-025 je podporená Islandom, Lichtenštajnskom a Nórskom prostredníctvom grantov EHP a Nórskych grantov.
Spoločným úsilím k zelenej, konkurencieschopnej a inkluzívnej Európe
Abstrakt
Formálne metódy majú potenciál výrazne zlepšiť kvalitu vyvíjaného softvéru, najmä tam, kde jeho chyby môžu viesť k vysokým a nákladným stratám. V praxi existuje viacero príkladov využitia formálnej verifikácie dokazovaním korektnosti softvéru, najmä v oblastiach kde prípadne zlyhanie softvéru predstavuje nie len finančné škody ale možné straty na životoch ako sú letecké systémy alebo medicína. Avšak formálne metódy nie sú široko používané v priemysle. Jedným z možných dôvodom tohto stavu je aj častá absencia ich výučby pred nástupom na univerzity. Študenti majú málo alebo žiadne predchádzajúce znalosti alebo skúsenosti, ktoré by mohli využiť pri predmetoch zameraných na formálnu logiku, teóriu typov, sémantiku alebo teóriu dôkazov. Avšak študenti informatiky sú vystavení mnohým predmetom zameraným na programovanie. Výučba logiky a formálnych metód z perspektívy programátora sa javí užitočným spôsobom nadobudnutia a osvojenia nových znalostí z oblasti teoretickej informatiky. Takýto prístup má potenciál pomôcť lepšie porozumieť a oceniť hodnotu takýchto metód, viesť k zlepšeniu kvality vyvinutého softvéru a zníženiu výskytu nákladných chýb.
Nástroje ako pokročilé textové editory, interpretery a podobné technológie sú užitočnými pomôckami pri učení sa nového programovacieho jazyka. Neustále poskytujú exaktnú spätnú väzbu programátorovi a tak eliminujú viacero výziev z komplexnosti programovania. Podobne môžu študenti profitovať z použitia takýchto nástrojov pri štúdiu teórie dôkazov v logike a sémantike. Hlavným cieľom tohto projektu bude vyvinúť softvér (výučbové nástroje), prostredníctvom ktorého budú študenti študovať základné princípy dedukcie a manipulácie s dôkazmi ako programami.
O nás
Výskumná skupina „Technológia programovania“ na Katedre informatiky, Univerzity v Osle (UiO) momentálne pripravuje predmet zameraný na pokročilé programovanie, sémantiku a teóriu typov. V tomto predmete budú študenti získavať hlbšie porozumenie teoretickým aspektom programovania tým, že budú implementovať základné koncepty programovacích jazykov, ako je interpreter a odvodenie typov.
Výskumná skupina “Teória programovania” na Katedre počítačov a informatiky, Fakulty elektrotechniky a informatiky, Technickej univerzity v Košiciach (TUKE) už vyučuje súvisiace predmety: Logika pre informatikov, Teória typov, Formálne jazyky a Sémantika programovacích jazykov.
Partneri na oboch univerzitách, TUKE a UiO, majú záujem o zatraktívnenie a zlepšenie výučby predmetov zameraných na teoretickú informatiku. V tomto bilaterálnom projekte budú TUKE a UiO zdieľať svoje skúsenosti pri výučbe logiky, teórie typov a sémantiky. Budeme spolupracovať na vytvorení nových výučbových materiálov pre obidve strany (nový predmet na UiO a existujúci predmet logiky na TUKE). Naším cieľom bude vyvinúť interaktívny výučbový nástroj a implementovať naše výsledky do výučbového procesu.