Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

First-order store and visibility in name-passing calculi

Daniel Hirschkoff, Iwan Quémerais, Davide Sangiorgi

TL;DR

This work formalises a visibility-based type system that constrains π-calculus computations to first-order store, drawing on game-semantic ideas to control how higher-order names reveal their services. By combining sequentiality and well-bracketing, the authors develop typed LTSs, traces, and labelled bisimulations that yield sound and complete characterisations of may-testing and barbed equivalence in both sequential and well-bracketed settings. The main contributions are a rigorous type-theoretic enforcement of first-order store and full abstractions for key behavioural equivalences, enabling precise reasoning about store and visibility in a pure name-passing language. The results have implications for security and predictability in concurrent languages and point to future extensions to richer storage models and free-output π-calculi.

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.

First-order store and visibility in name-passing calculi

TL;DR

This work formalises a visibility-based type system that constrains π-calculus computations to first-order store, drawing on game-semantic ideas to control how higher-order names reveal their services. By combining sequentiality and well-bracketing, the authors develop typed LTSs, traces, and labelled bisimulations that yield sound and complete characterisations of may-testing and barbed equivalence in both sequential and well-bracketed settings. The main contributions are a rigorous type-theoretic enforcement of first-order store and full abstractions for key behavioural equivalences, enabling precise reasoning about store and visibility in a pure name-passing language. The results have implications for security and predictability in concurrent languages and point to future extensions to richer storage models and free-output π-calculi.

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.

Paper Structure

This paper contains 20 sections, 28 theorems, 22 equations, 5 figures, 1 table.

Table of Contents

  1. Introduction
  2. Background: the $\pi$-calculus language
  3. A Type System for Visibility
  4. Labelled Semantics
  5. Trace-based proof techniques
  6. Visibility property on traces
  7. Adding Well-Bracketing
  8. Type system
  9. Labelled semantics
  10. Conclusions and Future Work
  11. Section \ref{['s:lang']}: Definition of the Operational Semantics
  12. Additional Material for Section \ref{['s:types']}
  13. Properties of the type system
  14. Properties of trace equivalence
  15. Pruning Processes using Types
  16. ...and 5 more sections

Key Result

Lemma 9

Suppose $\textcolor{green}{\Delta_1}\vdash P$, $\textcolor{green}{\Delta_1}\subseteq\textcolor{green}{\Delta_2}$, and ($\textcolor{green}{\Delta_2} \!\downharpoonleft\! \textcolor{pink}{\ast}$ iff $\textcolor{green}{\Delta_1} \!\downharpoonleft\! \textcolor{pink}{\ast}$). Then $\textcolor{green}{\

Figures (5)

  • Figure 1: Typing rules for visibility
  • Figure 2: Visible LTS
  • Figure 3: Typing rules with visibility and stack
  • Figure 4: Visible LTS with stack
  • Figure 5: Labelled transition semantics. Symmetric versions of the rules for parallel composition and for sum have been omitted.

Theorems & Definitions (55)

  • Definition 1: May testing
  • Definition 2: Barbed bisimilarity and equivalence
  • Definition 3: Visibility function
  • Example 4: Implicit forms of higher-order store
  • Remark 5: Transitivity and functional languages
  • Definition 6: Split
  • Example 7
  • Example 8
  • Lemma 9: Weakening
  • Theorem 10: Subject reduction
  • ...and 45 more