Home > Search Results: keywords:"teorie kvantitativních typů|obousměrné typování|typové systémy|lambda kalkulus|Haskell"
Search:
Search Tips :: Advanced Search
Search collections:
Sort by: Display results: Output format:
National Repository of Grey Literature 1 records found  Search took 0.01 seconds. 
Additive Pairs in Quantitative Type Theory
 Svoboda, Tomáš ; Šefl, Vít (advisor) ; Kratochvíl, Miroslav (referee)
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
Detailed record

Interested in being notified about new results for this query?
Subscribe to the RSS feed.
Digital Repository :: Search :: Submit :: Personalize :: Help
Powered by Invenio v1.1.2
Maintained by admin.invenio@techlib.cz
This site is also available in the following languages:
Česky  English