On Up-to Context Techniques in the $\pi$-calculus
Enguerrand Prebet (ENS Lyon, FOCUS)
TL;DR
This paper extends the theory of compatible functions to the pi-calculus, demonstrating that the up-to context proof technique for bisimulation remains compatible in specific variants of the calculus.
Contribution
It introduces a variant of compatible functions theory and proves the compatibility of the up-to context technique for bisimulation in two pi-calculus subsets.
Findings
Up-to context technique is compatible in asynchronous pi-calculus.
Compatibility also holds in pi-calculus with immediately available names.
Theoretical framework supports reasoning about process equivalences.
Abstract
We present a variant of the theory of compatible functions on relations, due to Sangiorgi and Pous. We show that the up-to context proof technique for bisimulation is compatible in this setting for two subsets of the pi-calculus: the asynchronous pi-calculus and a pi-calculus with immediately available names.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsAdvanced Algebra and Logic · Logic, Reasoning, and Knowledge · Logic, programming, and type systems