Master's thesis

Coinductive Formalization of SECD Machine in Agda

Bc. Adam Krupička
Abstract

V tejto práci formalizujeme SECD stroj v jazyku Agda. Za plného využitia závislých typov v tomto jazyku definujeme typovanú syntax inštrukcií pre SECD stroj. Potom definujeme sémantiku tohto stroja za použitia koindukcie. Nakoniec zavádzame λ kalkul, z ktorého definujeme kompilátor do SECD inštrukcií.

Abstract

In this thesis we give a formalization of SECD machine in a language called Agda. We take full advantage of the presence of dependent types in Agda and define typed assembly code for this machine. Then we give semantics to the typed assembly by the use of coinduction. Finally, we define a λ calculus and give a compilation procedure to SECD assembly, using a well-known approach.

Keywords
SECD Agda formalization coinduction
Thesis description
The aim of the thesis is to formalize Landin's Stack Environment Control Dump (SECD) machine in Agda. SECD machine is an interesting abstract machine that can serve as an compilation target for both typed and untyped lambda calculi. The formalization should contain both syntax of the SECD machine instructions and the semantics that formalize their evaluation. The implemented syntax should include a suitable type system and the implemented semantics will use coinduction. The thesis should contain introduction to Agda and its usage to formalize logical concepts and abstract machines. The thesis should also define and explain the SECD machine and provide introduction to the concept of coinduction. The thesis has to explain design choices that were made by the student during the formalization of the SECD machine.
Administrative information
The thesis has been checked:
17/12/2018 08:47, RNDr. Martin Jonáš, Ph.D., UČO 359542
Full text of thesis
252,2 KB / file PDF
Attachments (1)
Language used
English English
Defence date
8/2/2019
The thesis was defended successfully

Supervisor

RNDr. Martin Jonáš, Ph.D., UČO 359542
KTP FI MU

Reader

doc. Mgr. Jan Obdržálek, PhD., UČO 1552
KTP FI MU
Cite this text
Masaryk University Faculty of Informatics
Programme
Informatics
Field of Study

Theses on a related topic

List of theses with an identical keyword.

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