Obsah

• Teória vypočítateľnosti (pre programátorov)
• Formálna sémantika a teória správnosti
• Modely konkurentných systémov
• Funkcionálne programovanie
• Logické programovanie
• Interaktívne programovanie
• Formálne špecifikácie programov

• funkcie a čiastočné funkcie - projekcie, skladanie funkcií, trojice číslovacích (párovacích) funkcií
• univerzálne funkcie a čiastočné funkcie
• primitívne rekurzívne funkcie, rekurzívne funkcie a čiastočne rekurzívne (vypočítateľné) funkcie (na množine N)
• primitívne rekurzívne, rekurzívne a rekurzívne spočítateľné množiny a predikáty a ich vlastnosti
• výpočtové modely - Turingove stroje a iné modely
• ekvivalentnosť modelov vypočítateľnosti (rekurzívnosti a vypočítateľnosti na Turingovych strojoch)
• Churchova téza
• problém zastavenia a iné nerozhodnuteľné problémy
• kódovanie nečíslených oborov (oborov slov) do prirodzených čísiel

• sémantika imperatívnych jazykov (základné príkazy, príkaz skoku, volanie rekurzívne procedúry) - algebraická štruktúra sémantických domén, priama vs. "pokračovacia" sémantika (continuation)
• sémantika adresovania - sémantika blokov (prostredie vs. stav), modelovanie domén pre zložené dátové štruktúry
• sémantika beztypových funkcionálnych jazykov - lambda-kalkul, algebraická štruktúra domén, fixpointová sémantika, reflexívne domény, univerzálna doména
• sémantika nedeterministických konštrukcií - "relačná" fixpointová sémantika, Egli-Milnerova usporiadanie na reláciach (aproximácia)
• vlastnosti Hoareovských systémov (axiomatická sémantika) - zdravosť (korektnosť), resp. relatívna úplnosť systému
• najslabšia vstupná a najsilnejšia výstupná podmienka - syntaktická vs. sémantická charakterizácia, vyjadriteľnosť wp a sp
• porovnávanie operačnej, denotačnej a axiomatickej sémantiky

• kalkul CCS - zakladné konštruktory a princípy
• operačná sémantika CCS - značkované prechodové systémy, odvodzovacie pravidlá
• stopová sémantika a bisimulácia - definície a ich vzájomný vzťah
• vlastnosti bisimulácie - kongruentnosť, expanzná veta
• axiomatizácia bisimulácie - systémy axióm charakterizujúcich slabú a silnú bisimuláciu
• charakterizácia bisimulácie pomocou temporálnej logiky - popis logiky, charakterizačné vety
• Pi-kalkukus ako model pre mobile computing
• Petriho siete - základné definície a vlastnosti
• Henessy-Milner logic a modálny Mu-kalkulus

• základy lambda-kalkulu, syntax a sémantika
• syntax funkcionálneho jazyka (dátové štruktúry, preddefinované funkcie)
• metódy výpočtu funkcionálnych programov, výrazy a ich vyhodnocovanie (lenivé a striktné vyhodnocovanie)
• "abstrakcia" vo funkcionálnych jazykoch (polymorfizmus, funkcie vyšších rádov)
• typové vs. netypové funkcionálne jazyky
• metody návrhu funkcionálnych programov
• implementácia funkcionálnych jazykov, čistenie pamäti

• substitúcia a unifikácia, návrh a analýza unifikačného algoritmu, unifikácia v SLD-rezolúcii
• logické programy - Hornovské klauzuly, SLD-rezolúcia (výpočtový krok resp. dôkaz)
• dátové štruktúry v Prologu a základné operácie nad nimi (aritmetika, zoznamy, množiny, stromy, lesy, heap, prioritný front)
• výpočet logických programov - prologovské prehľadávanie do hĺbky, riadenie inferencie, "cut", dátové štruktúry (unárna aritmetika, zoznamy, stromy, lesy)
• sémantika logických programov - deklaratívna, modelová, fixpointová a operačná sémantika, vzajomné súvislosti, ekvivalencia
• prehľadávanie do hĺbky, prehľádavanie do šírky, práca s termami
• nedeterministické programovanie - technika backtracking producent/konzument
• logické programovanie druhého rádu
• princípy implementácie logických jazykov - metainterpretátory, Warenova abstraktná mašina
• logické programovanie s obmedzeniami - vzťah k CLP

• základné techniky interaktívneho programovania (HTTP, CGI, cookies, ASP, server side includes)
• programovacie jazyky na Internete, ich prehľad a využitie
• skriptovacie jazyky, základné princípy a využitie (JavaScript)
• Java, jej teoretický model a príncipy kompilovania, základné typy aplikácií (synchronizácia, sieťové spojenie a aplikácie typu point-to-point)
• princípy prepojenia webservrov a databázových servrov

• algebraická špecifikácia - signatúra a axiómy, algebraická špecifikácia v jazyku SL, modulárny návrh algebraickej špecifikácie (skladanie špecifikácií, parametrické špecifikácie), špecifikácia výnimočných a chybových stavov
• sémantika algebraickej špecifikácie - modely algebraickej špecifikácie, rôzne prístupy charakterizácie sémantiky algebraickej špecifikácie (iniciálna, voľná a behaviorálna sémantika), sémantické požiadavky pri skladaní špecifikácií (dostatočná úplnosť a konzistentnosť), hierarchická sémantika algebraickej špecifikácie
• konštruktívne algebraické špecifikácie - konštruktory, induktívny návrh axióm (pravidiel), výpočtový model algebraických špecifikácií (prepisovanie termov), kanonická špecifikácia
• implementácia špecifikácie - implementácia resp. behaviorálna implementácia špecifikácie
• ekvacionálna logika - ekvacionálne dokazovania v jednodruhovom, a mnohodruhovom prostredí, dokazovanie v induktívnych teóriách, dokazovanie behaviorálnych vlastností
• Z-špecifikácie - preddefinované typy v špecifikačnom jazyku Z (množiny, typy, logické funkcie a kvantifikátory, relácie a funkcie), špecifikačné schémy (skladanie špecifikácií, generické špecifikácie)
• postupné zjemnenie Z-špecifikácií, vývoj programu zo špecifikácií, princípy návrhu dátových štruktúr a algoritmov pomocou Z