First-order store and visibility in name-passing calculi
Fuente:
arXiv
Enregistré dans:
| Auteurs principaux: | , , |
|---|---|
| Format: | Preprint |
| Publié: |
2025
|
| Sujets: | |
| Accès en ligne: | |
| Tags: |
Ajouter un tag
Pas de tags, Soyez le premier à ajouter un tag!
|
| _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 |