Additive Types in Quantitative Type Theory
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F22%3A10447934" target="_blank" >RIV/00216208:11320/22:10447934 - isvavai.cz</a>
Result on the web
<a href="https://link.springer.com/chapter/10.1007/978-3-031-15298-6_16" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-031-15298-6_16</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-15298-6_16" target="_blank" >10.1007/978-3-031-15298-6_16</a>
Alternative languages
Result language
angličtina
Original language name
Additive Types in Quantitative Type Theory
Original language description
Dependent type theories enable us to reason about properties of our programs, while substructural type theories enable us to reason about their resource use. Quantitative type theory seamlessly combines dependent and substructural types by employing positive semirings to keep track of variable usage and computational contexts. Existing treatments of this theory typically focus on multiplicative connectives such as functions or multiplicative pairs. In this work, we extend quantitative type theory with additive zero, unit, unions and dependent pairs, as well as annotated eliminators for various types. We then explain how these additive types can be used to better describe resource use and how they integrate with existing programming techniques. Finally, we implement an interpreter for a language based on these extensions.
Czech name
—
Czech description
—
Classification
Type
D - Article in proceedings
CEP classification
—
OECD FORD branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Result continuities
Project
—
Continuities
S - Specificky vyzkum na vysokych skolach
Others
Publication year
2022
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Article name in the collection
Logic, Language, Information, and Computation
ISBN
978-3-031-15297-9
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
13
Pages from-to
250-262
Publisher name
Springer Nature
Place of publication
Switzerland
Event location
Iasi, Romania
Event date
Sep 20, 2022
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—