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
| Identifer | oai:union.ndltd.org:nusl.cz/oai:invenio.nusl.cz:448382 |
| Date | January 2021 |
| Creators | Svoboda, Tomáš |
| Contributors | Šefl, Vít, Kratochvíl, Miroslav |
| Source Sets | Czech ETDs |
| Language | English |
| Detected Language | English |
| Type | info:eu-repo/semantics/masterThesis |
| Rights | info:eu-repo/semantics/restrictedAccess |
Page generated in 0.0026 seconds