Doctoral thesis

Progress in Programming Language Semantics Frameworks

Mgr. Jan Tušil
Abstract

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 …more

Abstract

One can hardly imagine large-scale production of computer software without the use of high-level programming languages. These shield software engineers from the overwhelming amount of detail present in modern computer architectures: instruction sets, caches, out-of-order execution, and so on. But when these details are abstracted, what does remain of a programming language? When the remains – a programming …more

Keywords
formal semantics programming languages formal verification logic hyperproperties theorem proving Coq K-framework
Administrative information
The thesis has been checked:
7/2/2025 16:26, doc. Mgr. Jan Obdržálek, PhD., UČO 1552
Full text of thesis
1,1 MB / file PDF
Attachments (1)
Language used
English English
Defence date
12/6/2025
The thesis was defended successfully

Supervisor

doc. Mgr. Jan Obdržálek, PhD., UČO 1552
KTP FI MU

Readers

Prof. Dr. Alexander Knapp
University of Augsburg
Vlad Rusu, PhD
INRIA - CNRS, Lille
Cite this text
Masaryk University Faculty of Informatics
Programme
Plan
Computing Technology and Methodology

Theses on a related topic

List of theses with an identical keyword.

Similar documents

  • Přidání souboru

    Soubor nebo složku lze nahrát pomocí tlačítka Přidat.

  • Další operace se soubory

    Podrobnosti lze zjistit označením příslušného řádku.

  • Pohled pro experty

    Pro častou práci je možné zvolit režim Více možností.

  • Vyhledávání souborů

    Vyhledávaný výraz můžete zadat přímo do adresního řádku.

  • Rychlý přístup k souborům

    Pomocí funkce Nedávné je možné se rychle vrátit k právě prohlíženým souborům. Oblíbené soubory je také možné označit Hvězdičkou.