Absolvent si osvojí: princípy abstrakcie programov s cieľom analyzovať vlastnosti riadiacich štruktúr programov, nezávislé od konkrétnej interpretácie programu, princípy a metódy dokazovania správnosti programov, základné poznatky potrebné pre formálnu definíciu významu (sémantiky) impreratívnych a rekurzívnych programovacích jazykov.

Programové schémy: základné pojmy - štandardná schéma, interpretácia schémy, Herbrandove interpretácie, vlastnosti schém; rozhodnuteľnosť základných vlastností schém – základné výsledky o nerozhodnuteľnosti, podtriedy schém s rozhodnuteľnými vlastnosťami (voľné, Janovove schémy); porovnávanie a preklad tried schém - vzťahy medzi triedami štandardných, štruktúrovaných a rekurzívnych schém, čiastočne interpretované schémy.

Správnosť programov: čiastočná a totálna správnosť - invarianty a induktívne formuly, najslabšia vstupná a najsilnejšia výstupná podmienka; metódy dokazovania – Floydova metóda, Hoareovský dokazovací systém, indukčné techniky; systematický vývoj správnych programov.

Sémantika programov a jazykov: význam programu - princípy operačnej, denotačnej a axiomatickej sémantiky, sémantické domény – algebraická štruktúra, konštrukcia domén; formálna sémantika (operačný a denotačný význam) imperatívnych programov, porovnávanie operačnej a denotačnej sémantiky imperatívnych programov; formálna sémantika (operačný a denotačný význam) rekurzívnych funkcionálnych programov, porovnávanie operačnej a denotačnej sémantiky rekurzívnych programov, dokazovanie vlastností rekurzívnych programov.

Matematická teorie programů / Zohar Manna ; z amerického originálu přeložil Jiří Hořejš. Praha : Státní nakladatelství technické literatury, 1981
Prívara, I.: Úvod do teórie programovania, Učebné texty (verzia 2014 – pdf)