Programming with Dependent Additive Pairs

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

Výsledek na webu

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

Jazyk výsledku

angličtina

Název v původním jazyce

Programming with Dependent Additive Pairs

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

Programming with Dependent Additive Pairs

Popis výsledku anglicky

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.

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í

2025

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

Trends in Functional Programming

ISBN

978-3-031-74558-4

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

20

Strana od-do

92-111

Název nakladatele

Springer

Místo vydání

Cham

Místo konání akce

South Orange, New Jersey, USA

Datum konání akce

9. 1. 2024

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

WRD - Celosvětová akce

Kód UT WoS článku

—