Programming with Dependent Additive Pairs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216208%3A11320%2F25%3A10494163" target="_blank" >RIV/00216208:11320/25:10494163 - isvavai.cz</a>
Result on the web
<a href="https://doi.org/10.1007/978-3-031-74558-4_5" target="_blank" >https://doi.org/10.1007/978-3-031-74558-4_5</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-031-74558-4_5" target="_blank" >10.1007/978-3-031-74558-4_5</a>
Alternative languages
Result language
angličtina
Original language name
Programming with Dependent Additive Pairs
Original language description
Linear logic gives us additive pairs in the form of the additive conjunction. Intuitionistic type theory gives us dependent pairs in the form of the dependent sum type. What happens when we combine these two kinds of pairs together? And is this new pair type useful in practice? To answer these questions, we employ quantitative type theory, which can describe both substructural and dependent types simultaneously. In our previous work, we introduced dependent additive pairs. In this work, we show how these pairs can be used in three completely different scenarios: folding data structures using linear recursion schemes, computing resource-aware proofs, and defining additive versions of inductive and coinductive types. Each of these scenarios is then illustrated by an implementation in the Janus language.
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
2025
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
Trends in Functional Programming
ISBN
978-3-031-74558-4
ISSN
0302-9743
e-ISSN
1611-3349
Number of pages
20
Pages from-to
92-111
Publisher name
Springer
Place of publication
Cham
Event location
South Orange, New Jersey, USA
Event date
Jan 9, 2024
Type of event by nationality
WRD - Celosvětová akce
UT code for WoS article
—