Název: Aditivní dvojice v kvantitativní teorii typů
Překlad názvu: Additive Pairs in Quantitative Type Theory
Autoři: Svoboda, Tomáš ; Šefl, Vít (vedoucí práce) ; Kratochvíl, Miroslav (oponent)
Typ dokumentu: Diplomové práce
Rok: 2021
Jazyk: eng
Abstrakt: [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
Klíčová slova: teorie kvantitativních typů|obousměrné typování|typové systémy|lambda kalkulus|Haskell; quantitative type theory|bidirectional typing|type systems|lambda calculus|Haskell

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/127263

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


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