Typed Non-determinism in Functional and Concurrent Calculi

Bas van den Heuvel; Joseph W.N. Paulus; Daniele Nantes-Sobrinho; Jorge A. Pérez

doi:10.1007/978-981-99-8311-7_6

Typed Non-determinism in Functional and Concurrent Calculi

Bas van den Heuvel, Joseph W.N. Paulus, Daniele Nantes-Sobrinho, Jorge A. Pérez^*

^*Corresponding author for this work

Fundamental Computing

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

2 Citations (Scopus)

26 Downloads (Pure)

Abstract

We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a π -calculus with non-deterministic choice, governed by session types. Second, we introduce a resource λ -calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.

Original language	English
Title of host publication	Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings
Editors	Chung-Kil Hur
Place of Publication	Singapore
Publisher	Springer Science and Business Media Deutschland GmbH
Pages	112-132
Number of pages	21
ISBN (Electronic)	978-981-99-8311-7
ISBN (Print)	9789819983100
DOIs	https://doi.org/10.1007/978-981-99-8311-7_6
Publication status	Published - 2023
Event	21st Asian Symposium on Programming Languages and Systems, APLAS 2023 - Taipei, Taiwan Duration: 26-Nov-2023 → 29-Nov-2023

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	14405 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	21st Asian Symposium on Programming Languages and Systems, APLAS 2023
Country/Territory	Taiwan
City	Taipei
Period	26/11/2023 → 29/11/2023

Access to Document

10.1007/978-981-99-8311-7_6

Typed Non-determinism in Functional and Concurrent CalculiFinal publisher's version, 853 KBLicence: Taverne

Handle.net

Persistent link

Cite this

van den Heuvel, B., Paulus, J. W. N., Nantes-Sobrinho, D., & Pérez, J. A. (2023). Typed Non-determinism in Functional and Concurrent Calculi. In C.-K. Hur (Ed.), Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings (pp. 112-132). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14405 LNCS). Springer Science and Business Media Deutschland GmbH. https://doi.org/10.1007/978-981-99-8311-7_6

van den Heuvel, Bas ; Paulus, Joseph W.N. ; Nantes-Sobrinho, Daniele et al. / Typed Non-determinism in Functional and Concurrent Calculi. Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings. editor / Chung-Kil Hur. Singapore : Springer Science and Business Media Deutschland GmbH, 2023. pp. 112-132 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{22188354d1d74724b5b8248ac76a49bb,

title = "Typed Non-determinism in Functional and Concurrent Calculi",

abstract = "We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a π -calculus with non-deterministic choice, governed by session types. Second, we introduce a resource λ -calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.",

author = "{van den Heuvel}, Bas and Paulus, {Joseph W.N.} and Daniele Nantes-Sobrinho and P{\'e}rez, {Jorge A.}",

note = "Publisher Copyright: {\textcopyright} 2023, The Author(s), under exclusive license to Springer Nature Singapore Pte Ltd.; 21st Asian Symposium on Programming Languages and Systems, APLAS 2023 ; Conference date: 26-11-2023 Through 29-11-2023",

year = "2023",

doi = "10.1007/978-981-99-8311-7_6",

language = "English",

isbn = "9789819983100",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Science and Business Media Deutschland GmbH",

pages = "112--132",

editor = "Chung-Kil Hur",

booktitle = "Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings",

}

van den Heuvel, B, Paulus, JWN, Nantes-Sobrinho, D & Pérez, JA 2023, Typed Non-determinism in Functional and Concurrent Calculi. in C-K Hur (ed.), Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 14405 LNCS, Springer Science and Business Media Deutschland GmbH, Singapore, pp. 112-132, 21st Asian Symposium on Programming Languages and Systems, APLAS 2023, Taipei, Taiwan, 26/11/2023. https://doi.org/10.1007/978-981-99-8311-7_6

Typed Non-determinism in Functional and Concurrent Calculi. / van den Heuvel, Bas; Paulus, Joseph W.N.; Nantes-Sobrinho, Daniele et al.
Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings. ed. / Chung-Kil Hur. Singapore: Springer Science and Business Media Deutschland GmbH, 2023. p. 112-132 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 14405 LNCS).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › Academic › peer-review

TY - GEN

T1 - Typed Non-determinism in Functional and Concurrent Calculi

AU - van den Heuvel, Bas

AU - Paulus, Joseph W.N.

AU - Nantes-Sobrinho, Daniele

AU - Pérez, Jorge A.

PY - 2023

Y1 - 2023

N2 - We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a π -calculus with non-deterministic choice, governed by session types. Second, we introduce a resource λ -calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.

AB - We study functional and concurrent calculi with non-determinism, along with type systems to control resources based on linearity. The interplay between non-determinism and linearity is delicate: careless handling of branches can discard resources meant to be used exactly once. Here we go beyond prior work by considering non-determinism in its standard sense: once a branch is selected, the rest are discarded. Our technical contributions are three-fold. First, we introduce a π -calculus with non-deterministic choice, governed by session types. Second, we introduce a resource λ -calculus, governed by intersection types, in which non-determinism concerns fetching of resources from bags. Finally, we connect our two typed non-deterministic calculi via a correct translation.

UR - http://www.scopus.com/inward/record.url?scp=85178573388&partnerID=8YFLogxK

U2 - 10.1007/978-981-99-8311-7_6

DO - 10.1007/978-981-99-8311-7_6

M3 - Conference contribution

AN - SCOPUS:85178573388

SN - 9789819983100

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 112

EP - 132

BT - Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings

A2 - Hur, Chung-Kil

PB - Springer Science and Business Media Deutschland GmbH

CY - Singapore

T2 - 21st Asian Symposium on Programming Languages and Systems, APLAS 2023

Y2 - 26 November 2023 through 29 November 2023

ER -

van den Heuvel B, Paulus JWN, Nantes-Sobrinho D, Pérez JA. Typed Non-determinism in Functional and Concurrent Calculi. In Hur CK, editor, Programming Languages and Systems - 21st Asian Symposium, APLAS 2023, Proceedings. Singapore: Springer Science and Business Media Deutschland GmbH. 2023. p. 112-132. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-981-99-8311-7_6