2025/04/24 by Daniel Hirschkoff, Hirschkoff, Daniel, Iwan Quémerais +3
Computer Science · #Distributed and Parallel Computing Systems #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.2504.17350
openalex publication_date 2025/04/24 · openalex created_date 2025/10/18 · openalex updated_date 2026/07/28
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.