Pith. sign in

REVIEW 2 major objections 5 minor 60 references

Comparing Process Calculi Using Encodings

T0 review · 2 major / 5 minor · reviewed 2026-08-14 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read One relation can make encoding results comparable

desk verdict A useful survey of encodability criteria whose Section 5 overclaims the reach of its relation-based 'iff' characterizations; worth a referee pass to tighten the side conditions. read the letter →

arxiv 1908.08633 v1 pith:EHRKH36Z submitted 2019-08-23 cs.LO

Kirstin Peters (TU Berlin/TU Darmstadt) This is my paper · ORCID
classification cs.LO MSC 68Q85
keywords processcalculiencodingsencodabilitycriteriafullabstractionoperationalcorrespondenceexpressivenessseparationresultsbisimulation
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The reading

This paper is a survey of the many criteria used to judge whether an encoding from one process calculus into another is meaningful, and of the frameworks that try to unify them. It claims that the field is fragmented: because criteria and their variants are tailored to different settings, encodability and separation results are often incomparable, and it is not always clear that a criterion actually fits the setting in which it is used. The way out, the survey argues, is to translate every semantic criterion into a condition on the relation that an encoding induces between source terms and their translations, turning the problem of comparing criteria into the well-studied problem of comparing relations on processes. On this basis the paper reports that full abstraction alone, without fixed source and target equivalences, has very little semantic effect, while operational correspondence is exactly a bisimulation condition. A fair reader would care because a relation-based reading promises to make expressiveness hierarchies and separation proofs comparable across different calculi.

What carries the argument

The central device is the encoding-induced relation $R_{\llbracket\cdot\rrbracket} \subseteq (P_S \uplus P_T)^2$: the smallest relation containing $(S,\llbracket S\rrbracket)$ for every source term $S$. Each encodability criterion is reformulated as a property of such a relation (totality, transitivity, bisimulation-like simulation conditions, divergence reflection, success respect), so comparing criteria reduces to comparing relations on processes — a domain with a mature theory. The three iff-lemmas of [50] (full abstraction, operational correspondence, and a new correspondence simulation) do the bridge-work; correspondence simulation is the named new relation, intermediate between coupled similarity and bisimilarity, that captures weak operational correspondence.

What would settle it

A single counterexample within the machine-checked formalisation [51] — a pair of calculi and an encoding that is fully abstract with respect to preorders $R_S$ and $R_T$ but for which no transitive relation $R$ with $(S,\llbracket S\rrbracket)$ and $(\llbracket S\rrbracket,S)$ in $R$ and $R_S = R\upharpoonright P_S$, $R_T = R\upharpoonright P_T$ exists — would refute Lemma 5.1 and with it the claim that full abstraction imposes almost no semantic constraint. More broadly, producing any commonly used encodability criterion that cannot be expressed as a condition on the encoding-induced relation would falsify the paper's central methodological thesis.

Watch

Extended reading notes

Core claim

The paper's central claim is that the proliferation of encodability criteria — different criteria, different variants, fine-tuned to different settings — has made encodability and separation results in process calculi largely incomparable, and that the path to comparability is to map each criterion onto a condition on the relation between source and target terms induced by an encoding. For any encoding $\llbracket\cdot\rrbracket$ it defines the relation $R_{\llbracket\cdot\rrbracket} \subseteq (P_S \uplus P_T)^2$ that relates each source term to its literal translation; a criterion then becomes a property of such relations. Following the method of [50], full abstraction with respect to preorders $R_S$ and $R_T$ becomes exactly the existence of a transitive relation containing $(S,\llbracket S\rrbracket)$ and $(\llbracket S\rrbracket,S)$ whose restrictions are $R_S$ and $R_T$ — so, without fixing the equivalences, full abstraction says almost nothing. Operational correspondence becomes bisimilarity up to the target equivalence, and weak operational correspondence becomes a new notion, correspondence simulation, situated strictly between coupled similarity and bisimilarity. Thus the survey locates the semantic core of each commonly used criterion and makes criteria comparable as relations on processes.

Load-bearing premise

The decisive premise is that the three lemmas quoted from [50] really do capture full abstraction and (weak) operational correspondence as relation-based conditions, because this survey imports those lemmas without reproof and the Section 5 analysis stands or falls with them.

Editorial extensions

If this is right

  • Encodability and separation results proven under different criterion sets are incomparable, so building an expressiveness hierarchy requires fixing a single criterion set first.
  • Full abstraction without a fixed, canonical pair of equivalences imposes almost no semantic constraint; fully abstract encodings exist as soon as a transitive relation can combine the chosen source and target preorders.
  • Operational correspondence is exactly bisimilarity up to $\asymp_T$; its weak variant is exactly coupled similarity, so these criteria are simulation conditions in disguise.
  • In the five-criteria framework surveyed, a 'good' encoding is exactly one that relates source and target terms by a coupled simulation that reflects divergence and respects success.
  • Adding domain-specific criteria can strengthen encodability results but weakens separation results and makes comparison with existing results harder; they should be added only when necessary.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • Editorial inference: the relation-based mapping suggests a natural taxonomy project — classify every encodability criterion ever proposed by the class of relations it induces (reflexive, transitive, bisimulation-like, divergence-respecting), yielding a lattice of criteria and a principled way to choose them for a given expressiveness question.
  • Editorial inference: if the full-abstraction lemma is right, many published full-abstraction proofs carry less weight than their titles suggest; re-examining classical full-abstraction results (for instance encodings into the asynchronous $\pi$-calculus) through the relation-based lens could show which ones actually fix the equivalences enough to be informative.
  • Editorial inference: the method covers semantic criteria; extending it to structural criteria like compositionality and name invariance would require formalising contexts, and the paper explicitly leaves this open — a concrete next step would be to represent compositionality as a condition on the contextual closure of the induced relation.
  • Editorial inference: crediting the machine-checked formalisation [51] with the lemmas' correctness, the remaining risk is the gap between the abstract calculus model and real process calculi; testing the lemmas on calculi with unusual operators (such as the join-calculus) could reveal hidden assumptions.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

2 major / 5 minor

Summary. The paper is a short survey of encodability criteria used to compare process calculi. After setting up reduction semantics, encodings, and renaming policies, it surveys criteria under four headings: direct comparison via a behavioural relation, full abstraction, operational correspondence, and success/termination/barb preservation; it then covers structural criteria such as compositionality, name invariance, and homomorphic translation, and discusses a domain-specific criterion for preservation of distribution. Three general frameworks for unified notions of encoding quality are outlined: Gorla's five-criterion framework, Fu's theory of interaction, and van Glabbeek's theory of encodings. Section 5 presents the approach from [50] of mapping encodability criteria to conditions on the relation induced by the encoding, restating lemmas for full abstraction and (weak) operational correspondence. The paper concludes that criteria and variants are incomparable, that frameworks differ, and that formal analysis of criteria is still incomplete.

Significance. This is a useful expository paper for the EXPRESS/SOS audience. Its main contribution is a structured taxonomy of criteria, with explicit definitions, and a comparative discussion of existing general frameworks. The paper honestly attributes the formal results of Section 5 to [50] and points to the Isabelle/HOL formalization [51], which is machine-checked; this is a genuine strength. If the relation-based characterizations are correct under suitable side conditions, they provide a promising model-independent way to compare criteria and to identify the semantic content of full abstraction and operational correspondence. However, the formal claims in Section 5 are not fully supported as written: the lemmas are stated for restricted classes of target preorders that are absent from the criteria of Section 3, and one key notion is left undefined. These gaps are load-bearing for the paper's methodological claim and need to be repaired.

major comments (2)
  1. [Section 5, Lemma 5.2 and preceding paragraph] The claim that the first two variants of Definition 3.1 "exactly describe" strong and weak bisimilarity up to ≍T is too strong. Definition 3.1 does not require ≍T to be a preorder, let alone a bisimulation; Lemma 5.2 only applies to encodings that are operationally corresponding w.r.t. a preorder ≍T that is itself a bisimulation. This is a substantive side condition, not a notational convenience. A concrete instance showing the gap: let PS={S,S'} with S⇒S', PT={C1,C1',C2} with C1⇒C1' and C2 inert, and set enc(S)=C1, enc(S')=C1', and ≍T to the reflexive closure of {(C1,C2)}. This encoding satisfies the sound and complete clauses of operational correspondence from Definition 3.1, yet no relation R with R↾PT=≍T can be a bisimulation, since C2 cannot match the step C1⇒C1'. Thus Lemma 5.2 does not capture Definition 3.1 as written. The text should either strengthen Definition 3.1 explicitly or qualify the "exactly" claim and state the restricted scope of Lemma 5.2.
  2. [Section 5, Lemma 5.3] The lemma's right-hand side refers to "correspondence simulation", but the paper explicitly says "We omit the definition of correspondence simulation". As a result, the claimed characterization of weak operational correspondence is uncheckable from the paper alone, and the conclusion that weak operational correspondence ensures coupled similarity rests on an undefined concept. The definition, or a precise statement of the lemma from [50], should be included together with the conditions under which it applies before this part of the central claim can be assessed.
minor comments (5)
  1. [Section 3.2 and Section 5, Lemma 5.1] Definition 3.2 defines full abstraction with respect to two behavioural equivalences, while Lemma 5.1 states the characterization for preorders; the text should clarify whether preorders are intended as a generalization or as a different criterion, since the two formulations do not literally coincide.
  2. [Section 3.3, Definition 3.1] The prose preceding Definition 3.1 calls ≍T "some equivalence on the target language", but the formal definition only states ≍T ⊆ P_T^2 and imposes no reflexivity, transitivity, or symmetry requirement; the prose and the formal definition should be aligned.
  3. [Section 3.6, Definition 3.5] The discussion immediately after Definition 3.5 claims that when a component Si can reduce on its own, its translation Ti can emulate the reduction modulo ≍T; this derivative-emulation property is not part of Definition 3.5 as stated and appears to come from a combination with operational completeness rather than from the definition alone.
  4. [Section 5, introductory paragraph] The paper says the relation-based mapping "completely capture[s]" the semantic effect of criteria, but the lemmas are imported from [50] without proof sketches; a brief note that full proofs and the Isabelle/HOL formalization appear in [50,51] would help the reader calibrate the strength of the claims.
  5. [Page 1, running header] The running header reads "EXPRES S/SOS" and should read "EXPRESS/SOS".

Circularity Check

0 steps flagged · score 1.0 of 10

No significant circularity: the survey's central incomparability claim is independently supported, and the relation-based characterizations imported from the author's prior work are backed by a machine-checked Isabelle/HOL formalization.

full rationale

Walking the claimed derivation chain: the main thesis, that different encodability criteria and their variants yield incomparable results, is supported by external literature (for example [43, 41, 45, 22] and the full-abstraction discussion citing [13, 23, 46]), not by the author's own prior work. Section 5's mapping of criteria to relation conditions is not re-derived here; it is explicitly imported from [50] and formalized in [51]. Because [51] is an Isabelle/HOL formalization in the Archive of Formal Proofs, the cited lemmas count as machine-checked independent support under the review rules, so the self-citation is not load-bearing circularity. Two imprecisions should be weighed: Lemma 5.2 requires the target preorder to be a bisimulation, a side condition absent from Definition 3.1, and Lemma 5.3 invokes 'correspondence simulation' without giving its definition, since the paper states 'We omit the definition of correspondence simulation but point out that it is a simulation relation that is in between coupled similarity and bisimulation.' These are correctness and completeness limitations of the survey, not reductions of a conclusion to its own input: no equation in the paper is identical to its assumptions by construction, and no fitted value is renamed as a prediction. Therefore no circular step is established.

Assumptions & free parameters 0 free parameters · 3 assumptions · 0 invented entities

The paper introduces no fitted parameters or invented entities. Its central claims rest on the standard definitions of process calculi, on the correctness of the cited frameworks, and on the author's prior lemmas, the latter supported by the Isabelle/HOL formalization [51].

assumptions (3)
  • domain assumption Process calculi are modeled as (PC, ↦→C) with reduction semantics; labelled semantics are not the default setting.
    Section 2 states: 'Here we assume that the semantics of the language is provided as a reduction semantics, because in the context of encodings the treatment of reductions is simpler.' This restricts the scope of the survey's formal analysis.
  • domain assumption Lemma 5.1, 5.2, and 5.3 from [50] correctly characterize the semantic effects of full abstraction and operational correspondence.
    Section 5 restates these lemmas from the author's prior paper and uses them to conclude that full abstraction without fixed equivalences has small semantic effect and that weak operational correspondence yields coupled similarity. The paper does not reprove them here; it cites [50] and its Isabelle/HOL formalization [51].
  • domain assumption The selected encodability criteria and frameworks are representative of the field.
    The survey is explicitly a 'short survey' (Section 1) and does not prove coverage; conclusions about incomparability of results are based on the selected literature.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Comparing Process Calculi Using Encodings." pith.science (2026). https://pith.science/paper/EHRKH36Z

@misc{pith2026190808633,
  author       = {Pith},
  title        = {Pith review of: Comparing Process Calculi Using Encodings},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/EHRKH36Z}},
  note         = {Machine review of arXiv:1908.08633}
}
read the original abstract

Encodings or the proof of their absence are the main way to compare process calculi. To analyse the quality of encodings and to rule out trivial or meaningless encodings, they are augmented with encodability criteria. There exists a bunch of different criteria and different variants of criteria in order to reason in different settings. This leads to incomparable results. Moreover, it is not always clear whether the criteria used to obtain a result in a particular setting do indeed fit to this setting. This paper provides a short survey on often used encodability criteria, general frameworks that try to provide a unified notion of the quality of an encoding, and methods to analyse and compare encodability criteria.

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

60 extracted references · 28 canonical work pages

  1. [50]

    Peters & R

    K. Peters & R. van Glabbeek (2015): Analysing and Comparing Encodability Criteria . In: Proc. of EX- PRESS/SOS, EPTCS 190, pp. 46–60, doi:10.4204/EPTCS.190.4

    doi:10.4204/eptcs.190.4 2015

  2. [51]

    Peters & R

    K. Peters & R. van Glabbeek (2015): Analysing and Comparing Encodability Criteria for Process Calculi. Archive of Formal Proofs . http://isa-afp.org/entries/Encodability_Process_Cal culi.shtml

    work page 2015

  3. [1]

    Arun-Kummar & M

    S. Arun-Kummar & M. Hennessy (1992): An efficiency preorder for processes . Acta Informatica 29(8), pp. 737–760, doi:10.1007/BF01191894

    work page doi:10.1007/bf01191894 1992

  4. [2]

    Baeten (2005): A brief history of process algebra

    J.C.M. Baeten (2005): A brief history of process algebra . Theoretical Computer Science 335(2–3), pp. 131–146, doi:10.1016/j.tcs.2004.07.036

    doi:10.1016/j.tcs.2004.07.036 2005

  5. [3]

    Baldamus, J

    M. Baldamus, J. Parrow & B. Victor (2005): A Fully Abstract Encoding of the π -Calculus with Data T erms (Extended Abstract). In: Proc. of ICALP, LNCS 3580, Springer, pp. 1202–1213, doi:10.1007/11523468 97

    doi:10.1007/11523468 2005

  6. [4]

    Bergstra & J.W

    J.A. Bergstra & J.W . Klop (1982): Fixed point semantics in process algebra . Technical Report IW 206/82, Mathematical Centre, Amsterdam

    work page 1982

  7. [5]

    Boer & C

    F.S. Boer & C. Palamidessi (1991): Embedding as a tool for Language Comparison: On the CSP hiera rchy. In: Proc. of CONCUR, LNCS 527, Springer, pp. 127–141, doi:10.1007/3-540-54430-5 85

    work page doi:10.1007/3-540-54430-5 1991

  8. [6]

    Boudol (1992): Asynchrony and the π -calculus (note)

    G. Boudol (1992): Asynchrony and the π -calculus (note). Note, INRIA

    work page 1992

Show all 60 references
  1. [7]

    Buckley & A

    G.N. Buckley & A. Silberschatz (1983): An Effective Implementation for the Generalized Input-Out put Con- struct of CSP . ACM Transactions on Programming Languages and Systems (TOP LAS) 5(2), pp. 223–235, doi:10.1145/69624.357208

    1983

  2. [8]

    N. Busi, M. Gabbrielli & G. Zavattaro (2009): On the expressive power of recursion, replication and iteration in process calculi . Mathematical Structures in Computer Science 19(6), pp. 1191–1222, doi:10.1017/S096012950999017X

    2009 doi

  3. [9]

    Cacciagrano, F

    D. Cacciagrano, F. Corradini, J. Aranda & F.D. V alencia (2008): Linearity, Persistence and T esting Semantics in the Asynchronous Pi-Calculus . Electronic Notes in Theoretical Computer Science 194(2), pp. 59–84, doi:10.1016/j.entcs.2007.11.006

    2008 doi

  4. [10]

    Carbone & S

    M. Carbone & S. Maffeis (2003): On the Expressive Power of Polyadic Synchronisation in π -Calculus. Nordic Journal of Computing 10(2), pp. 70–98, doi:10.1016/S1571-0661(05)80361-5

    2003 doi

  5. [11]

    Fournet & G

    C. Fournet & G. Gonthier (1996): The Reflexive CHAM and the Join-Calculus . In: Proc. of POPL, SIGPLAN- SIGACT, ACM, pp. 372–385, doi:10.1145/237721.237805

    1996

  6. [12]

    Fu (2016): Theory of Interaction

    Y . Fu (2016): Theory of Interaction . Theoretical Computer Science 611, pp. 1–49, doi:10.1016/j.tcs.2015.07.043

    2016 doi

  7. [13]

    Y . Fu & H. Lu (2010): On the expressiveness of interaction . Theoretical Computer Science 411(11-13), pp. 1387–1451, doi:10.1016/j.tcs.2009.11.011

    2010 doi

  8. [14]

    van Glabbeek (1993): The Linear Time – Branching Time Spectrum II

    R.J. van Glabbeek (1993): The Linear Time – Branching Time Spectrum II . In: Proc. of CONCUR , LNCS 715, pp. 66–81, doi:10.1007/3-540-57208-2 6

    1993 doi

  9. [15]

    van Glabbeek (1994): On the expressiveness of ACP (extended abstract)

    R.J. van Glabbeek (1994): On the expressiveness of ACP (extended abstract) . In: Proc. of ACP, Workshops in Computing, pp. 188–217, doi:10.1007/978-1-4471-2120- 6 8

    1994 doi

  10. [16]

    van Glabbeek (2001): The Linear Time – Branching Time Spectrum I: The Semantics of Conrete, Se- quential Processes

    R.J. van Glabbeek (2001): The Linear Time – Branching Time Spectrum I: The Semantics of Conrete, Se- quential Processes. Handbook of Process Algebra , pp. 3–99, doi:10.1016/B978-044482830-9/50019-9

    2001 doi

  11. [17]

    van Glabbeek (2012): Musings on Encodings and Expressiveness

    R.J. van Glabbeek (2012): Musings on Encodings and Expressiveness . In: Proc. of EXPRESS/SOS , EPTCS 89, pp. 81–98, doi:10.4204/EPTCS.89.7

    2012 doi

  12. [18]

    van Glabbeek (2018): A Theory of Encodings and Expressiveness (Extended Abstrac t)

    R.J. van Glabbeek (2018): A Theory of Encodings and Expressiveness (Extended Abstrac t). In: Proc. of FoSSaCS, LNCS 10803, pp. 183–202, doi:10.1007/978-3-319-89366-2 10

    2018 doi

  13. [19]

    Gorla (2008): T owards a Unified Approach to Encodability and Separation Re sults for Process Calculi

    D. Gorla (2008): T owards a Unified Approach to Encodability and Separation Re sults for Process Calculi . In: Proc. of CONCUR, LNCS 5201, pp. 492–507, doi:10.1007/978-3-540-85361-9 38

    2008 doi

  14. [20]

    Gorla (2009): On the Relative Expressive Power of Calculi for Mobility

    D. Gorla (2009): On the Relative Expressive Power of Calculi for Mobility . In: Proc. of MFPS, ENTCS 249, pp. 269–286, doi:10.1016/j.entcs.2009.07.094

    2009 doi

  15. [21]

    Gorla (2010): A taxonomy of process calculi for distribution and mobility

    D. Gorla (2010): A taxonomy of process calculi for distribution and mobility . Distributed Computing 23(4), pp. 273–299, doi:10.1007/s00446-010-0120-6. K. Peters 37

    2010 doi

  16. [22]

    Gorla (2010): T owards a Unified Approach to Encodability and Separation Re sults for Process Calculi

    D. Gorla (2010): T owards a Unified Approach to Encodability and Separation Re sults for Process Calculi . Information and Computation 208(9), pp. 1031–1053, doi:10.1016/j.ic.2010.05.002

    2010 doi

  17. [23]

    Gorla & U

    D. Gorla & U. Nestmann (2014): Full abstraction for expressiveness: history, myths and fa cts. Mathematical Structures in Computer Science , pp. 1–16, doi:10.1017/S0960129514000279

    2014 doi

  18. [24]

    Hatzel, C

    M. Hatzel, C. Wagner, K. Peters & U. Nestmann (2015): Encoding CSP into CCS . In: Proc. of EX- PRESS/SOS, EPTCS 7, pp. 61–75, doi:10.4204/EPTCS.190.5

    2015 doi

  19. [25]

    Hewitt, P

    C. Hewitt, P . Bishop & R. Steiger (1973): A universal modular ACTOR formalism for artificial intellig ence. In: Proc. of IJCAI , ACM, pp. 235–245

    1973

  20. [26]

    Hoare (1978): Communicating Sequential Processes

    C.A.R. Hoare (1978): Communicating Sequential Processes. Communications of the ACM 21(8), pp. 666– 677, doi:10.1145/359576.359585

    1978

  21. [27]

    Honda & M

    K. Honda & M. Tokoro (1991): An Object Calculus for Asynchronous Communication . In: Proc. of ECOOP, LNCS 512, pp. 133–147, doi:10.1007/BFb0057019

    1991 doi

  22. [28]

    Honda & N

    K. Honda & N. Y oshida (1995): On Reduction-Based Process Semantics . Theoretical Computer Science 151(2), pp. 437–486, doi:10.1016/0304-3975(95)00074-7

    1995 doi

  23. [29]

    Knabe (1993): A Distributed Protocol for Channel-Based Communication wi th Choice

    F. Knabe (1993): A Distributed Protocol for Channel-Based Communication wi th Choice . Computers and Artificial Intelligence 12(5), pp. 475–490

    1993

  24. [30]

    Laneve & A

    C. Laneve & A. Vitale (2010): The Expressive Power of Synchronizations . In: Proc. of LICS , IEEE, pp. 382–391, doi:10.1109/LICS.2010.15

    2010 doi

  25. [31]

    Lipton, L

    R.J. Lipton, L. Snyder & Y . Zalcstein (1974): A Comparative Study of Models of Parallel Computation . In: Proc. of SW A T, IEEE, pp. 145–155, doi:10.1109/SW A T.1974.2

    1974 doi

  26. [32]

    Milner (1989): Communication and Concurrency

    R. Milner (1989): Communication and Concurrency. Prentice-Hall, Inc

    1989

  27. [33]

    Milner (1992): Functions as Processes

    R. Milner (1992): Functions as Processes. Mathematical Structures in Computer Science 2(2), pp. 119–141, doi:10.1017/S0960129500001407

    1992 doi

  28. [34]

    Milner (1993): The Polyadic π -Calculus: a Tutorial

    R. Milner (1993): The Polyadic π -Calculus: a Tutorial. Logic and Algebra of Specification 94, pp. 203–246, doi:10.1007/978-3-642-58041-3 6

    1993 doi

  29. [35]

    Milner (1999): Communicating and Mobile Systems: The π -Calculus

    R. Milner (1999): Communicating and Mobile Systems: The π -Calculus. Cambridge University Press, New Y ork

    1999

  30. [36]

    Milner, J

    R. Milner, J. Parrow & D. Walker (1992): A Calculus of Mobile Processes, Part I and II . Information and Computation 100(1), pp. 1–77, doi:10.1016/0890-5401(92)90008-4

    1992 doi

  31. [37]

    Milner & D

    R. Milner & D. Sangiorgi (1992): Barbed Bisimulation . In: Proc. of ICALP , LNCS 623, pp. 685–695, doi:10.1007/3-540-55719-9 114

    1992 doi

  32. [38]

    Mitchell (1993): On abstraction and the expressive power of programming lang uages

    J.C. Mitchell (1993): On abstraction and the expressive power of programming lang uages. Science of Computer Programming 21(2), pp. 141–163, doi:10.1016/0167-6423(93)90004-9

    1993 doi

  33. [39]

    Nestmann (1996): On Determinacy and Nondeterminacy in Concurrent Programmi ng

    U. Nestmann (1996): On Determinacy and Nondeterminacy in Concurrent Programmi ng. Ph.D. thesis, Universit¨ at Erlangen-N¨ urnberg

    1996

  34. [40]

    Nestmann (2000): What is a “Good” Encoding of Guarded Choice? Information and Computation 156(1-2), pp

    U. Nestmann (2000): What is a “Good” Encoding of Guarded Choice? Information and Computation 156(1-2), pp. 287–319, doi:10.1006/inco.1999.2822

    2000

  35. [41]

    Nestmann (2006): W elcome to the Jungle: A subjective Guide to Mobile Process C alculi

    U. Nestmann (2006): W elcome to the Jungle: A subjective Guide to Mobile Process C alculi. In: Proc. of CONCUR, LNCS 4137, pp. 52–63, doi:10.1007/11817949 4

    2006 doi

  36. [42]

    Nestmann & B.C

    U. Nestmann & B.C. Pierce (2000): Decoding Choice Encodings . Information and Computation 163(1), pp. 1–59, doi:10.1006/inco.2000.2868

    2000

  37. [43]

    Palamidessi (2003): Comparing the Expressive Power of the Synchronous and the Asynchronous π -calculi

    C. Palamidessi (2003): Comparing the Expressive Power of the Synchronous and the Asynchronous π -calculi. Mathematical Structures in Computer Science 13(5), pp. 685–719, doi:10.1017/S0960129503004043

    2003 doi

  38. [44]

    Palamidessi, V .A

    C. Palamidessi, V .A. Saraswat, F.D. V alencia & B. Victo r (2006): On the Expressiveness of Linearity vs Persistence in the Asychronous Pi-Calculus . In: Proc. of LICS , IEEE Computer Society, pp. 59–68, doi:10.1109/LICS.2006.39. 38 Comparing Process Calculi Using Encodings

    2006 doi

  39. [45]

    Parrow (2008): Expressiveness of Process Algebras

    J. Parrow (2008): Expressiveness of Process Algebras . Electronic Notes in Theoretical Computer Science 209, pp. 173–186, doi:10.1016/j.entcs.2008.04.011

    2008 doi

  40. [46]

    Parrow (2014): General conditions for full abstraction

    J. Parrow (2014): General conditions for full abstraction . Mathematical Structures in Computer Science 26(4), pp. 655–657, doi:10.1017/S0960129514000280

    2014 doi

  41. [47]

    Parrow & P

    J. Parrow & P . Sj¨ odin (1992): Multiway Synchronization V erified with Coupled Simulation . In: Proc. of CONCUR, LNCS 630, pp. 518–533, doi:10.1007/BFb0084813

    1992 doi

  42. [48]

    Perez (2009): Higher-Order Concurrency: Expressiveness and Decidabili ty Results

    J.A. Perez (2009): Higher-Order Concurrency: Expressiveness and Decidabili ty Results. Ph.d. thesis, Uni- versity of Bologna

    2009

  43. [49]

    Peters (2012): Translational Expressiveness

    K. Peters (2012): Translational Expressiveness . Ph.D. thesis, TU Berlin. Available at http://opus.kobv.de/tuberlin/volltexte/2012/3749/

    2012

  44. [52]

    Peters & U

    K. Peters & U. Nestmann (2012): Is It a “Good” Encoding of Mixed Choice? In: Proc. of FoSSaCS , LNCS 7213, pp. 210–224, doi:10.1007/978-3-642-28729-9 14

    2012 doi

  45. [53]

    Peters, U

    K. Peters, U. Nestmann & U. Goltz (2013): On Distributability in Process Calculi. In: Proc. of ESOP, LNCS 7792, pp. 310–329, doi:10.1007/978-3-642-37036-6 18

    2013 doi

  46. [54]

    Petri (1962): Kommunikation mit Automaten

    C.A. Petri (1962): Kommunikation mit Automaten . Ph.D. thesis, Institut f¨ ur Instrumentelle Mathematik, Bonn

    1962

  47. [55]

    Riecke (1991): Fully abstract translations between functional languages

    J.G. Riecke (1991): Fully abstract translations between functional languages . In: Proc. of POPL, ACM, pp. 245–254, doi:10.1145/99583.99617

    1991

  48. [56]

    Sangiorgi (1994): An investigation into functions as processes

    D. Sangiorgi (1994): An investigation into functions as processes . In: Proc. of MFPS , LNCS 802, pp. 143– 159, doi:10.1007/3-540-58027-1 7

    1994 doi

  49. [57]

    Sangiorgi (2009): On the Origins of Bisimulation and Coinduction

    D. Sangiorgi (2009): On the Origins of Bisimulation and Coinduction . ACM Transactions on Programming Languages and Systems (TOPLAS) 31(4), pp. 1–15, doi:10.1145/1516507.1516510

    2009

  50. [58]

    Victor & J

    B. Victor & J. Parrow (1996): Constraints as Processes. In: Proc. of CONCUR , LNCS 1119, pp. 389–405, doi:10.1007/3-540-61604-7 66

    1996 doi

  51. [59]

    Vigliotti, I

    M.G. Vigliotti, I. Phillips & C. Palamidessi (2007): Tutorial on separation results in process calculi via leader election problems. Theoretical Computer Science 388(1–3), pp. 267–289, doi:10.1016/j.tcs.2007.09.001

    2007 doi

  52. [60]

    Y oshida (1996): Graph Types for Monadic Mobile Processes

    N. Y oshida (1996): Graph Types for Monadic Mobile Processes . In: Proc. of FST&TCS , LNCS 1180, pp. 371–386, doi:10.1007/3-540-62034-6 64

    1996 doi

Pith tools

Reviewed August 14, 2026 · model on record in the stance chip above.