First-order store and visibility in name-passing calculi
Logic in Computer Science
2025-04-25 v1
Abstract
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.
Cite
@article{arxiv.2504.17350,
title = {First-order store and visibility in name-passing calculi},
author = {Daniel Hirschkoff and Iwan Quémerais and Davide Sangiorgi},
journal= {arXiv preprint arXiv:2504.17350},
year = {2025}
}