Original title: Aditivní dvojice v kvantitativní teorii typů
Translated title: Additive Pairs in Quantitative Type Theory
Authors: Svoboda, Tomáš ; Šefl, Vít (advisor) ; Kratochvíl, Miroslav (referee)
Document type: Master’s theses
Year: 2021
Language: eng
Abstract: [eng] [cze]
Both dependent types and linear types have their desirable properties. Department types can express functional dependencies of inputs and outputs, while linear types offer control over the use of computational resources. Combining these two systems have been difficult because of their different interpretations of context presence of variables. Quantitative Type Theory (QTT) combines dependent types and linear types by using a semiring to track the kind of use of every resource. We extend QTT with the additive pair and additive unit types, express the complete QTT rules in bidirectional form, and then present our interpreter of a simple language based on QTT. 1 Jan závislé, tak lineární typy mají své kýžené vlastnosti. Zatímco závislé typy mo- hou vyjádřit závislosti mezi vstupy a výstupy funkcí, lineární typy umožňují kontrolu nad používáním zdrojů. Kombinace těchto dvou systémů byla složitá kvůli dvou různým interpretacím výskytu proměnné v kontextu. Teorie kvantitativních typů (QTT) kom- binuje závislé a lineární typy použitím polookruhů ke sledování druhů spotřeby každé proměnné. Tato práce rozšiřuje QTT o aditivní páry a aditivní jednotky, formuluje kompletní QTT pravidla ve formě oboustranného typování, a prezentuje náš interpret jednoduchého jazyka založeného na QTT. 1
Keywords: quantitative type theory|bidirectional typing|type systems|lambda calculus|Haskell; teorie kvantitativních typů|obousměrné typování|typové systémy|lambda kalkulus|Haskell

Institution: Charles University Faculties (theses) (web)
Document availability information: Available in the Charles University Digital Repository.
Original record: http://hdl.handle.net/20.500.11956/127263

Permalink: http://www.nusl.cz/ntk/nusl-448382


The record appears in these collections:
Universities and colleges > Public universities > Charles University > Charles University Faculties (theses)
Academic theses (ETDs) > Master’s theses