zbMATH — the first resource for mathematics

A sorted semantic framework for applied process calculi (extended abstract). (English) Zbl 1348.68158
Abadi, Martín (ed.) et al., Trustworthy global computing. 8th international symposium, TGC 2013, Buenos Aires, Argentina, August 30–31, 2013. Revised selected papers. Cham: Springer (ISBN 978-3-319-05118-5/pbk; 978-3-319-05119-2/ebook). Lecture Notes in Computer Science 8358, 103-118 (2014).
Summary: Applied process calculi include advanced programming constructs such as type systems, communication with pattern matching, encryption primitives, concurrent constraints, nondeterminism, process creation, and dynamic connection topologies. Several such formalisms, e.g. the applied pi calculus, are extensions of the the pi-calculus; a growing number is geared towards particular applications or computational paradigms.
Our goal is a unified framework to represent different process calculi and notions of computation. To this end, we extend our previous work on psi-calculi with novel abstract patterns and pattern matching, and add sorts to the data term language, giving sufficient criteria for subject reduction to hold. Our framework can accommodate several existing process calculi; the resulting transition systems are isomorphic to the originals up to strong bisimulation. We also demonstrate different notions of computation on data terms, including cryptographic primitives and a lambda-calculus with erratic choice. Substantial parts of the meta-theory of sorted psi-calculi have been machine-checked using Nominal Isabelle.
For the entire collection see [Zbl 1334.68011].

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
Full Text: DOI