Additive Pairs in Quantitative Type Theory
| Název práce v češtině: | Aditivní dvojice v kvantitativní teorii typů |
|---|---|
| Název v anglickém jazyce: | Additive Pairs in Quantitative Type Theory |
| Klíčová slova: | teorie kvantitativních typů|obousměrné typování|typové systémy|lambda kalkulus|Haskell |
| Klíčová slova anglicky: | quantitative type theory|bidirectional typing|type systems|lambda calculus|Haskell |
| Akademický rok vypsání: | 2019/2020 |
| Typ práce: | diplomová práce |
| Jazyk práce: | angličtina |
| Ústav: | Katedra algebry (32-KA) |
| Vedoucí / školitel: | Mgr. Vít Šefl, Ph.D. |
| Řešitel: | skrytý - zadáno a potvrzeno stud. odd. |
| Datum přihlášení: | 25.08.2020 |
| Datum zadání: | 25.08.2020 |
| Datum potvrzení stud. oddělením: | 11.09.2020 |
| Datum a čas obhajoby: | 21.06.2021 09:00 |
| Datum odevzdání elektronické podoby: | 22.05.2021 |
| Datum odevzdání tištěné podoby: | 22.05.2021 |
| Datum proběhlé obhajoby: | 21.06.2021 |
| Oponenti: | RNDr. Miroslav Kratochvíl, Ph.D. |
| Zásady pro vypracování |
| Teorie závislých typů kombinuje programování s dokazováním. Tento přístup ale vede ke ztrátě informace o účelu dat, což zabraňuje rozlišení mezi použitím ve formulaci typů a použitím při výpočtu. Kvantitativní teorie typů (QTT) kombinuje závislé typy s lineární logikou a pro reprezentaci účelu dat používá polookruhy [3, 1].
Diplomová práce má za úkol modifikovat existující implementaci jednoduchého programovacího jazyka se závislými typy [2] tak, aby ke kontrole typů používal pravidla QTT, a přidat formulaci aditivních dvojic. Aditivní dvojice umožňují modelování zdrojů tak, že všechny dostupné zdroje mohou být využity prvním, nebo druhým prvkem dvojice, nikoli však oběma zároveň. |
| Seznam odborné literatury |
| [1] Robert Atkey. The Syntax and Semantics of Quantitative Type Theory. In LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, July 9--12, 2018, Oxford, United Kingdom. 2018.
[2] Andres Löh, Conor McBride, Wouter Swierstra. A Tutorial Implementation of a Dependently Typed Lambda Calculus. Fundamenta Informaticae. April 2010. [3] Conor McBride. I Got Plenty o' Nuttin'. A List of Successes That Can Change the World 2016: 207-233 [4] Edwin Brady. Idris 2: Quantitative Type Theory in Action. https://www.type-driven.org.uk/edwinb/papers/idris2.pdf |