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

Type theory and its semantics

Bc. Vít Jelínek, učo 485180
Anotace

V práci zkoumáme kategorie s reprezentovatelnými šipkami (CwRs) -- potenciální odpověď na otázku "Co je to (závislá) teorie typů?" navrženou Taichim Uemurou v jeho dizertační práci. Dokazujeme, že 2-kategorie všech CwRs má různé dobré 2-kategoriální vlastnosti -- jedná se o dosažitelnou 2-kategorii s flexibilními limitami a bikolimitami. Díky těmto vlastnostem můžeme CwRs volně generovat kategoriemi …více

Abstract

We examine categories with representable maps (CwRs) -- an answer to the question `What is a (dependent) type theory?' suggested by Taichi Uemura in his PhD thesis. We prove that the 2-category of CwRs has various good 2-categorical properties -- it is an accessible 2-category with flexible limits and bicolimits. Using this, we deduce that CwRs can be freely generated by categories with specified arrows …více

Klíčová slova
type theory semantics 2-category theory logic bicolimits teorie typů sémantika 2-kategorie logika bikolimity
Zadání práce
The thesis is devoted to semantics of dependent type theory. Specifically, it should examine categories with representable maps (CwR) developed by Taichi Uemura. These can serve as a unified definition of dependent type theories, and enable also a unified definition of semantics. In particular, the main topics to be investigated are various construction of type theories. The student ought to show how (potentially) complicated type theories are generated by simpler data, and, moreover, explain how the constructed type theories are related to semantics of the simpler data. Usage of these techniques on a concrete examples should be demonstrated. The student will also explain connections of CwRs with traditional approaches to semantics.
Administrativní informace
Práce zkontrolována:
22. 5. 2024 10:55, doc. John Denis Bourke, PhD, učo 115440
Plný text práce
646,4 KB / soubor PDF
Jazyk práce
angličtina angličtina
Termín obhajoby
21. 6. 2024
Práce byla úspěšně obhájena

Vedoucí

doc. John Denis Bourke, PhD, učo 115440
ÚMS Ústavy PřF MU

Oponent

doc. Benno Van den Berg, PhD
Institute for Logic, Language and Computation, University of Amsterdam
Citovat tuto práci
Masarykova univerzita Fakulta informatiky
Studijní program
Plán
Diskrétní algoritmy a modely

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.