Diplomová práce
Získaná ocenění: Cena děkana FI za vynikající závěrečnou práci

An Executable Formal Semantics of Agda

Bc. Andrej Tokarčík
Anotace

Agda je aktívne vyvíjaný programovací jazyk so závislými typmi a interaktívny dokazovač matematických viet založený na upravenej teórii typov Martin-Löfa. V práci je predstavená spustiteľná formálna sémantika časti tohto jazyka vytvorená pomocou sémantického frameworku K. Diskutujú sa jednak otázky týkajúce sa formalizácie Agdy a druhak kľúčové rozhodnutia učinené počas vývoja jej sémantiky. Základom …více

Abstract

Agda is an actively developed dependently typed programming language and interactive theorem prover based on a variant of Martin-Löf type theory. This thesis presents an executable formal semantics of a portion of the language, created using the K semantic framework. Issues pertaining to formalisation of Agda as well as the key decisions made during the development of the semantics are discussed. …více

Klíčová slova
K Agda KAgda formal semantics operational semantics rewriting logic type theory dependent type systems formálna sémantika operačná sémantika prepisovacia logika teória typov typové systémy so závislými typmi
Zadání práce
Agda is an actively developed dependently typed functional programming language and interactive theorem prover based on a variant of Martin-Löf type theory. The thesis objective is to describe a fragment of this language – focusing primarily on Agda’s type system extended with mechanisms for introduction of data types and inductive families – in the K semantic framework. In the thesis the student should:
  • examine and discuss issues regarding formalisation of the chosen features of Agda (in general as well as with respect to K in particular)
  • present an executable formal semantics of the fragment of Agda written in K.
The author should also provide an exposition of the related type-theoretic concepts and briefly demonstrate relevant capabilities of both Agda and K.
Administrativní informace
Práce zkontrolována:
26. 5. 2015 11:37, doc. Mgr. Jan Obdržálek, PhD., učo 1552
Plný text práce
385,7 KB / soubor PDF
Přílohy (1)
Jazyk práce
angličtina angličtina
Termín obhajoby
25. 6. 2015
Práce byla úspěšně obhájena

Vedoucí

doc. Mgr. Jan Obdržálek, PhD., učo 1552
ITI FI MU

Oponent

doc. RNDr. Tomáš Brázdil, Ph.D., MBA, učo 4074
KSUZD FI MU

Literatura

  • NORELL, Ulf. Towards a practical programming language based on dependent type theory. Göteborg, Sweden: Chalmers University, 2007.
  • ROŞU, Grigore a Traian FLORIN ŞERBĂNUȚĂ. An overview of the K semantic framework. Journal of Logic and Algebraic Programming. Holland: Elsevier, 2010, roč. 79, č. 6, s. 397–434. ISSN 1567-8326.
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Informatika
Obor

Práce na příbuzné téma

Seznam prací, které mají shodná klíčová slova.

Podobné práce

  • 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.