Additive Types in Quantitative Type Theory

Kód výsledku v 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>

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Additive Types in Quantitative Type Theory

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Additive Types in Quantitative Type Theory

Popis výsledku anglicky

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.

Druh

D - Stať ve sborníku

CEP obor

—

OECD FORD obor

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Projekt

—

Návaznosti

S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2022

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Název statě ve sborníku

Logic, Language, Information, and Computation

ISBN

978-3-031-15297-9

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

13

Strana od-do

250-262

Název nakladatele

Springer Nature

Místo vydání

Switzerland

Místo konání akce

Iasi, Romania

Datum konání akce

20. 9. 2022

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

—