Představa masové produkce počítačového software bez použití
vysokoúrovňových programovacích jazyků je obtížná. Tyto jazyky
odstiňují softwarové inženýry od detailů přítomných v moderních
počítačových architekturách: instrukční sady, keše, provádění
instrukcí mimo pořadí, a tak dále. Ale když se abstrahujeme od
těchto detailů, co zbyde z programovacího jazyka?

Když tyto "zbytky" - sémantiku daného programovacího jazyka -
přesně popíšeme, důležité otázky začnou dávat smysl: otázky
typu "Je tento překladač korektní?" či "Může můj program
selhat?". Můžeme však jít ještě dále: s jednotným konceptem
"sémantiky" sdílené mezi jazyky, vývoj programovacích jazyků se
zjednodušší a zautomatizuje. Například je možné napsat
interpreter nebo deduktivní verifikátor takovým způsobem, že
tento je parametrický v sémantice cílového programovacího
jazyka, a následně získat interpreter nebo verifikátor pro
libovolný jazyk popsaný uvnitř takovéhoto frameworku téměř
zadarmo.

Tato práce představuje tři příspěvky k vývoji frameworků pro
sémantiky programovacích jazyků. Prvním příspěvkem je Cartesian
Reachability Logic (CRL) - programová logika pro uvažování o
třídě hypervlastností programů psaných v libovolném
deterministickém jazyce s formální sémantikou určitého
(operačního) druhu. CRK rozšiřuje předchozí práci na
jazykově-parametrických programových logikách, stejně jako
práci na logikách pro hypervlastnosti. Druhým příspěvkem je
důkazový systém typu přirozené dedukce pro "logiku shody"
(matching logic) - logiky použité pro ospravedlnění chování
existujícího frameworku pro programovací jazyky (K-framework).
Tento důkazový ssystém je doprovázen praktickou implementací
prostředí pro dokazování tvrzení ("proof mode") vestavěném v
důkazovém asistentu Coq. Třetím príspěvkem je návrh, vývoj, a
formální verifikace nástroje zvaného Minuska - nového,
praktického frameworku pro sémantiky programovacích jazyků
schoného odvozovat interpretery z operačních sémantik.
Interpretery generované Minuskou jsou výkonné a poskytují
silnější garance než interpretery generované K-frameworkem;
navíc návrh Minusky obhází jisté problémy s korektností
přítomné v K-frameworku.