Salvato in:
| Autori principali: | , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2025
|
| Soggetti: | |
| Accesso online: | https://arxiv.org/abs/2504.17350 |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866916705710637056 |
|---|---|
| author | Hirschkoff, Daniel Quémerais, Iwan Sangiorgi, Davide |
| author_facet | Hirschkoff, Daniel Quémerais, Iwan Sangiorgi, Davide |
| contents | The $π$-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how $π$-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2504_17350 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | First-order store and visibility in name-passing calculi Hirschkoff, Daniel Quémerais, Iwan Sangiorgi, Davide Logic in Computer Science The $π$-calculus is the paradigmatical name-passing calculus. While being purely name-passing, it allows the representation of higher-order functions and store. We study how $π$-calculus processes can be controlled so that computations can only involve storage of first-order values. The discipline is enforced by a type system that is based on the notion of visibility, coming from game semantics. We discuss the impact of visibility on the behavioural theory. We propose characterisations of may-testing and barbed equivalence, based on (variants of) trace equivalence and labelled bisimilarity, in the case where computation is sequential, and in the case where computation is well-bracketed. |
| title | First-order store and visibility in name-passing calculi |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2504.17350 |