Název: On the semantics of exceptions for high level and low level languages
Překlad názvu: On the semantics of exceptions for high level and low level languages
Autoři: Tejiščák, Matúš ; Swierstra, Wouter (vedoucí práce) ; Kučera, Petr (oponent)
Typ dokumentu: Diplomové práce
Rok: 2012
Jazyk: eng
Abstrakt: [eng] [cze]
The thesis deals with correctness of a compiler of a simple language featuring exceptions. We present formal semantics, both denotational semantics of a~high-level language and operational semantics of a low-level language for a~simple stack machine. We study the method of stack unwinding and then iteratively, improving upon a naive solution, we present a different method that is structurally recursive and thus suitable for implementation in total dependently typed languages. Finally, we provide an implementation of the compiler in the dependently typed functional programming language Agda, along with a mechanically verifiable proof of adherence of the implementation to the semantics. V práci se zabýváme korektností kompilátoru jazyka s výjimkami. Předkládáme formální sémantiku; jak denotační sémantiku vysokoúrovňového jazyka, tak operační sémantiku jazyka instrukcí pro zásobníkový stroj. Studujeme metodu odvíjení zásobníku a poté, iterativně ve více krocích, předkládáme modifikovanou metodu. Tato je strukturálně rekurzivní a tudíž vhodná pro implementaci v totálních závisle typovaných jazycích. Nakonec předkládáme implementaci kompilátoru v závisle typovaném jazyce Agda, spolu se strojově ověřitelným důkazem, že předložená implementace kompilátoru při překladu zachovává sémantiku programu.
Klíčová slova: certifikovaný kompilátor; korektnost; výjimky; závisle typované programování; certified compiler; correctness; dependently-typed programming; exceptions

Instituce: Fakulty UK (VŠKP) (web)
Informace o dostupnosti dokumentu: Dostupné v digitálním repozitáři UK.
Původní záznam: http://hdl.handle.net/20.500.11956/40801

Trvalý odkaz NUŠL: http://www.nusl.cz/ntk/nusl-305104


Záznam je zařazen do těchto sbírek:
Školství > Veřejné vysoké školy > Univerzita Karlova > Fakulty UK (VŠKP)
Vysokoškolské kvalifikační práce > Diplomové práce