Pith. sign in

REVIEW 4 major objections 4 minor 160 references

Constructive characterisations of the must-preorder for asynchrony

T0 review · 4 major / 4 minor · reviewed 2026-08-10 · deepseek-v4-flash

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

Pith's one-line read The standard characterisations of the must-preorder survive asynchrony once servers act as forwarders.

desk verdict A substantial, mostly machine-checked result with an important mismatch between the prose theorems and the Coq statement: the completeness direction needs client-generator hypotheses that are not guaranteed for all Fdb LTSs. read the letter →

arxiv 2501.13002 v1 pith:NKPLBY2E submitted 2025-01-22 cs.LO cs.PL

Giovanni Bernardi , Ilaria Castellani , Paul Laforgue , Léo Stefanesco This is my paper · ORCID
classification cs.LOcs.PL MSC 68Q8503B35
keywords must-preorderasynchronouscommunicationacceptancesetsmust-setscoinductivepreorderforwardersbarinductionCoqmechanisation
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 establishes that the classic behavioural characterisations of De Nicola and Hennessy's must-preorder --- acceptance sets, must-sets, and the coinductive preorder --- are sound and complete for asynchronous communication, provided each server is first lifted to a "forwarding" version that can read any message as long as it stores it back into the shared mailbox. Since the must-preorder quantifies over all possible clients, it is not a workable proof method on its own; the characterisations turn it into a comparison of observable behaviour on a single labelled transition system. The result is calculus-independent: it is proved for Selinger's output-buffered agents with feedback, the general LTS class covering asynchronous CCS and the asynchronous pi-calculus, and it is fully mechanised in Coq. The development is constructive, using Brouwer's bar induction to relate the extensional definition of "must" to an inductive one. As corollaries, the must-preorder coincides with failure-divergence refinement, and a normal form that ignores non-causal action orderings also characterises it.

What carries the argument

The load-bearing construction is the forwarder lift $FW$, which maps any output-buffered agent with feedback $L = \langle A, L, \to\rangle$ to an LTS whose states are pairs $p \vartriangleright M$ of a process and a finite multiset of messages in a shared mailbox. Four rules govern it: the process may move alone; an input may synchronise with a matching message in the mailbox; the whole state may input any message into the mailbox; and it may output any message from the mailbox. This makes every state input-enabled, with each input looping back through a complementary output --- exactly the behaviour of a forwarder that receives a message and stores it back. The lift preserves the must predicate (Lemma 3), places the LTS in the class Fwd where acceptance sets can be simplified to sets of outputs, and leaves the standard alternative preorders unchanged, so the complexity of asynchrony is absorbed by the LTS rather than by the definitions.

What would settle it

Take a finite Fdb LTS whose only client state is stable, non-successful, and has no outgoing transitions, while two servers differ in their reachable output sets. Then $p \sqsubseteq_{\mathrm{must}} q$ holds vacuously (no client can make $p$ succeed), yet $FW(p) \preceq_{AS} FW(q)$ fails if the servers' stable output sets are incomparable; such a pair would show the unqualified Theorem 1 fails without the $tc$ and $ta$ hypotheses.

Watch

Extended reading notes

Core claim

The paper's central claim is Theorem 1: for every LTS $L_A, L_B$ in the class Fdb and every servers $p, q$, $p \sqsubseteq_{\mathrm{must}} q$ holds exactly when $FW(p)$ is below $FW(q)$ in the standard acceptance-set preorder $\preceq_{AS}$, where $FW$ is the forwarder lift pairing each process with a multiset mailbox. The same comparison also characterises the preorder through must-sets (Theorem 3) and through a single-action coinductive preorder $\preceq_{\mathrm{co}}$ (Theorem 2), which gives a practical proof method and is used to certify a code-hoisting transformation. The paper shows, contrary to earlier calculus-specific work, that the alternative preorders themselves need no adjustment: only the LTS is enhanced, so the same definitions work for synchronous and asynchronous semantics. Along the way it proves that the intensional (inductive) and extensional versions of termination and "must" coincide using decidable bar induction, and it reports the first fully mechanised, fully nondeterministic theory of the must-preorder in Coq.

Load-bearing premise

The completeness direction assumes that the asynchronous LTS at hand can express the two client generators $tc$ and $ta$ with the properties listed in Table 1 --- one that tests convergence along traces, one that tests acceptance sets --- because the main text states Theorem 1 for every Fdb LTS, while the mechanised statement carries these as explicit hypotheses and Appendix D notes their existence depends on the LTS at hand.

Editorial extensions

If this is right

  • For any calculus whose LTS is in Fdb and can express the two client generators, proving a refinement reduces to comparing acceptance sets on the forwarder-lifted LTS, with no calculus-specific machinery.
  • The coinductive preorder gives a single-action proof method; the paper uses it to certify the code-hoisting refinement $\tau.(\bar a \parallel b) + \tau.(\bar a \parallel c) \sqsubseteq_{\mathrm{must}} \bar a \parallel (\tau.b + \tau.c)$.
  • The must-preorder coincides with failure-divergence refinement: $p \sqsubseteq_{\mathrm{must}} q$ iff $FW(p) \preceq_{\mathrm{cnv}} FW(q)$ and $FW(p) \le_{\mathrm{fail}} FW(q)$ (Corollary 3).
  • Normalising traces into multisets of consecutive inputs and outputs yields a preorder on normal forms that again characterises the must-preorder (Corollary 4), so irrelevant action orderings can be dropped in proofs.
  • Because all statements are mechanised in Coq, the characterisations are reusable as a library for machine-checked liveness-preserving transformations in message-passing languages.

Reading between the lines

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

  • The forwarder construction is a general recipe for transferring synchronous testing theories to asynchronous ones: any calculus with an Fdb LTS inherits the standard characterisations, and the same lift may apply to may-preorder, fair testing, or compliance.
  • Adopting these theorems in a new calculus leaves one concrete task unautomated: constructing the convergence and acceptance client generators; the paper supplies them for ACCS, and their absence would void the characterisation.
  • The normal-form result suggests a testable extension to ordered media: replacing the order-insensitive normal form with queue-respecting traces should yield the analogous characterisation for FIFO or per-channel mailboxes, with the forwarder axioms adjusted accordingly.
  • A finite counterexample of the kind described under falsifier would settle whether the main-text Theorem 1 overstates the mechanised theorem; if it exists, the effective statement is the hypothesised one.
Share X Bluesky LinkedIn Reddit HN

Editorial analysis

A structured set of objections, weighed in public.

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

Referee Report

4 major / 4 minor

Summary. The paper studies De Nicola and Hennessy's must-preorder for asynchronous systems modelled as Selinger output-buffered agents with feedback (the class Fdb). Its central claim is that the standard characterisations of the must-preorder carry over unchanged to asynchrony provided each server is enhanced with a forwarding construction FW: Theorem 1 states that for all LTSs LA, LB in Fdb and all servers p, q, p is must-below q if and only if FW(p) is below FW(q) in the acceptance-set preorder; Theorem 3 gives the analogous must-set characterisation, and Theorem 2 gives a coinductive characterisation on image-finite LTSs. The development is mechanised in Coq, uses a conversion between extensional and intensional liveness predicates via bar induction, introduces an auxiliary predicate mustaux on sets of servers, and demonstrates the coinductive preorder on a code-hoisting example. The paper also contains a counterexample to a previously published completeness result for asynchronous CCS.

Significance. If the main theorem is correct with a suitable statement, this is a significant contribution: it provides the first calculus-independent account of the must-preorder for asynchrony, shows that the standard acceptance-set, must-set, and coinductive preorders need no modification once forwarding is added, and supplies a substantial machine-checked Coq development with an archived artifact. The methodological choices are also valuable: the LTS-of-sets construction, the explicit use of bar induction for liveness reasoning, and the disclosure of the underlying axioms are all strong points. The proof of the code-hoisting example gives evidence that the coinductive characterisation is practically usable. However, the printed Theorem 1 is stronger than the mechanised theorem, and this mismatch affects the paper's headline claim of a characterisation for every Fdb LTS.

major comments (4)
  1. [§3.1, Theorem 1; Appendix D, Table 1; Appendix J.6] Theorem 1 is stated as an equivalence for every LA, LB ∈ Fdb, but the Coq statement equivalence_bhv_acc_ctx shown in Appendix J.6 is proved inside a section whose hypotheses include FiniteLts A L, FiniteLts B L, gen_spec_conv gen_conv, and gen_spec_acc gen_acc. Appendix D explicitly says that the existence of the client-generating functions tc and ta satisfying Table 1 depends on the LTS at hand, and concrete definitions are given only for ACCS in Appendix H.2. No construction of these generators from the Fdb axioms is supplied. Consequently, the completeness direction (Proposition 4 / Lemma 20) is established only for Fdb instances that are finite in the sense of the Coq typeclass and that can express convergence tests and acceptance-set tests. Since Theorem 1 is the linchpin from which Theorem 3, Corollary 4, and the normal-form characterisation are derived, the missing hypotheses propagate. The theorem statements, the abstract's 'calculus-independent' claim, and the contribution list need to be amended to include these hypotheses, or a proof that every Fdb LTS admits such generators must be provided.
  2. [Appendix D, Lemma 20; Appendix H.2] The proof of Lemma 20 uses the set E = ⋃ Afw(p, s) and then applies Lemma 19 with the set X = E \ O, where O is a ready set of q. Lemma 19 is stated only for a finite set O, and the test generator ta defined in Appendix H.2 forms a finite product Π{μ.1 | μ ∈ L}, so it is only well defined for finite L. The Fdb axioms guarantee that each individual set O(p') is finite, but they do not guarantee that the union over all stable states reachable after a trace is finite. The Coq statement's FiniteLts hypothesis would provide such finiteness, but the printed theorem omits it. This is a load-bearing gap in the completeness proof as written, and it reinforces the need to state Theorem 1 with the mechanised hypotheses.
  3. [§3.3, Theorem 2; §3.1, Theorem 1] Theorem 2 is stated for image-finite LTSs, but its proof relies on Theorem 1, which is stated without any image-finiteness or FiniteLts hypothesis. The reader is left with inconsistent assumptions between the two central theorems. The paper should either make Theorem 1's hypotheses explicit and then state Theorem 2 as a consequence under the same hypotheses, or explain why Theorem 2 can be derived without the finiteness assumptions that the mechanised completeness proof requires.
  4. [§3.2, Proposition 1; Appendix B.1; Abstract] The paper advertises a 'constructive account' of the must-preorder, but the equivalence between the extensional and intensional predicates (Corollary 2) depends on Proposition 1, decidable bar induction over an STS, which is postulated as an axiom and proved in Coq using the ClassicalEpsilon axiom. The authors disclose this in §3.2 and argue admissibility, but the abstract and contribution list state the development is constructive without this qualification. The claim should be restated as constructive relative to bar induction / ClassicalEpsilon, or the proof of bar induction in the base type theory should be supplied. This is not a fatal flaw, but it is part of the paper's central novelty claim.
minor comments (4)
  1. [Appendix E, proof of Lemma 37] The proof contains the placeholder identifier 'pattaboy' in several equations; this should be replaced with a proper variable name.
  2. [Appendix J.2, Coq snippet] The notation line 'p − →[α] q' is defined with 'lts_step p (ActExt µ) q', where the binder µ is not the same as α; the displayed notation and the definition should use a consistent action variable.
  3. [Appendix D, first paragraph] The sentence 'whether such tc and ta can actually exist' is important but easy to miss; it should be highlighted in the main text near Theorem 1, since it determines the actual scope of the characterisation.
  4. [§3.2, paragraph on admissibility] The phrase 'since it is not provable directly in the type theory of Coq' could be misread as saying bar induction is inconsistent with Coq; consider rephrasing to 'not derivable in the current set-theoretic/type-theoretic formalisation'.

Circularity Check

0 steps flagged · score 0.0 of 10

No circularity found: the acceptance-set, must-set and coinductive preorders are defined independently of the contextual must-preorder, and the extra client-generator hypotheses in the Coq development are explicit stated limitations rather than conclusions assumed in the proof.

full rationale

The paper's central theorems equate the contextual must-preorder with independently defined behavioural preorders: ≼_AS (Definition 5), ≼_MS (Definition 13), and ≼_co (Definition 12). None of these definitions mentions the must-preorder or is parameterized by it, so the claimed equivalences are not definitionally forced. The completeness direction uses client generators tc and ta, and Appendix D explicitly says "whether such tc and ta can actually exist depends on the LTS at hand"; the Coq statement of Theorem 1 (Section J.6) includes hypotheses gen_spec_conv and gen_spec_acc. This is a real scope gap between the prose quantification over all Fdb LTSs and the mechanized theorem, but it is not circularity: the hypotheses are additional expressiveness assumptions about the LTS, not restatements of the conclusion, and the paper does not rename fitted data as predictions. Self-citations to De Nicola and Hennessy, Selinger, and Honda and Tokoro supply background definitions and inspiration for forwarding, but the main soundness and completeness proofs are carried out in the paper and in Coq rather than reduced to those citations. The use of bar induction is also not circular: it is posited as an admissible principle and used to relate extensional and intensional predicates, not used to assume the preorder characterization. Overall, the derivation chain is self-contained against external benchmarks, and the notable weakness is an over-general statement of Theorem 1, which belongs to correctness risk, not circularity.

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

No free parameters are fitted to data. The central claims rest on the Fdb model class, the good-invariance assumption, the existence of test clients, and the bar-induction principle. Forwarders are a definable construction on LTSs rather than a postulated empirical entity.

assumptions (5)
  • domain assumption LTSs are output-buffered agents with feedback (Fdb), obeying the axioms in Figure 2, including Backward-output-determinacy.
    The whole theory is stated for this class of LTSs; if a calculus does not satisfy these axioms, the theorems do not apply.
  • domain assumption The success predicate good is invariant under output transitions (Equation 4).
    Used to propagate success across client outputs in Lemmas 13 and 14; if outputs could erase success, the characterisations would need revision.
  • domain assumption Client generators tc and ta with the properties in Table 1 exist.
    Completeness constructs tests from traces and acceptance sets; existence depends on the LTS and is represented by gen_spec_conv and gen_spec_acc in the Coq development.
  • ad hoc to paper Decidable bar induction over an STS (Proposition 1).
    Used to identify extensional and intensional must and termination; not primitive in Coq and is derived from ClassicalEpsilon, so it is an extra proof principle.
  • domain assumption Countably branching STS with a surjection from natural numbers to the reducts of each state, after sink enrichment.
    Needed to transport bar induction from natural-number sequences to executions; valid for ACCS and usual calculi but not for every Fdb LTS.

how reviews work

0 comments
Cite this review

Pith. "Pith review of Constructive characterisations of the must-preorder for asynchrony." pith.science (2026). https://pith.science/paper/NKPLBY2E

@misc{pith2026250113002,
  author       = {Pith},
  title        = {Pith review of: Constructive characterisations of the must-preorder for asynchrony},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/NKPLBY2E}},
  note         = {Machine review of arXiv:2501.13002}
}
read the original abstract

De Nicola and Hennessy's must-preorder is a contextual refinement which states that a server q refines a server p if all clients satisfied by p are also satisfied by q. Owing to the universal quantification over clients, this definition does not yield a practical proof method for the must-preorder, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions. We show that the standard characterisations of the must-preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Coq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous pi-calculus. We show that the standard coinductive characterisation lets us prove in Coq that concrete programs are related by the must-preorder. Finally, our proofs show that Brouwer's bar induction principle is a useful technique to reason on liveness preserving program transformations.

Figures

Figures reproduced from arXiv: 2501.13002 by the authors.

Figure 1
Figure 1. The behaviours of a server p0 and of a client r0. to either output a string, or input an integer. The input int makes the client move to the successful state r2, while the output str makes the client move to the state r1, where it can still perform the input int to reach the successful state r3. In an asynchronous setting, output transitions enjoy a commutativity property on which we will return later. Programs p ar… view at source ↗
Figure 2
Figure 2. First-order axioms for output-buffered agents with feedback as given by Selinger [90], extended with the Backward-output-determinacy axiom. Asynchrony In distributed systems, communication is inherently asynchronous. For instance, the standard TCP transmission on the Internet is asynchronous. Actor languages like Elixir and Erlang implement asynchrony via mailboxes, and both Python and JavaScript offer developers th… view at source ↗
Figure 3
Figure 3. Highlights of our Sts and Lts typeclasses. 2 Preliminaries We model individual programs such as servers p and clients r as LTSs obeying Selinger axioms, while client-server systems p V r are modelled as state transi￾tion systems with a reduction semantics. We now formally define this two-level semantics. Labelled transition systems A labelled transition system (LTS) is a triple L = hA, L, −→i where A is the set of s… view at source ↗
Figures from the paper (15 more)
Figure 4
Figure 4. Figure 4: The STS of server-client systems. is finite for any p. In our mechanisation, the set O(p) is rendered by the function lts_outputs, and we shall also use a function lts_performs that lets us decide whether a state can perform a transition labelled by a given action. Cli…
Figure 5
Figure 5. Figure 5: Axiom stating that equivalence ≃ is compatible with a transition relation. Definition 4 (Transition sequence). Given an LTS hA, L, −→i and a state p0 ∈ A, a transition sequence of p0 is a finite or infinite sequence of the form p0α1p1α2p2 · · · with pi ∈ A and αi ∈ L, …
Figure 6
Figure 6. Figure 6: Lifting of an LTS to an LTS with forwarding. Let us briefly comment on Definition 6 and the rules in [PITH_FULL_IMAGE:figures/full_fig_p013_6.png]
Figure 7
Figure 7. Figure 7: Rules to define inductively the predicate mustaux. Lemma 7. For every LTSs LA,LB and every set of servers X ∈ P+(A), we have that X mustaux r if and only if for every p ∈ X. p musti r. The LTS of sets has two important applications in this paper: first, it is used to d…
Figure 8
Figure 8. Figure 8: The state transition system of client-server system. p V r X X X. . . τ τ τ τ τ τ τ p V r X X X. . . τ τ τ τ τ τ τ p V r X X X. . . τ τ τ τ τ τ τ (1) (2) (3) [PITH_FULL_IMAGE:figures/full_fig_p036_8.png]
Figure 9
Figure 9. Figure 9: Extensional approach: finding successful prefixes in every maximal path of the computational tree. The extensional approach To prove p must r, the extensional definition of must requires checking that every maximal path in the tree in [PITH_FULL_IMAGE:figures/full_fig…
Figure 10
Figure 10. Figure 10: Intensional approach: visiting the tree bottom-up, starting from the bar. The intensional approach Consider now the predicate musti - which is defined intensional ly - and a proof that p musti r. The base case of musti ensures that all the nodes that contain a success…
Figure 11
Figure 11. Figure 11: An infinite branching computational tree where the bar X is at unbounded depth. mately leads to the same outcomes. In our setting this amounts to proving that the predicates must and musti are logically equivalent, and similarly for the convergence predicates ↓ and ↓i…
Figure 12
Figure 12. Figure 12: Definition of the trace normalisation function nf 2. If (10) corresponds to a transition of the process, it must be that µ = a and q = τ.b + τ.c ⊲ M. In that case, the set X′ of processes reached from {τ.(a k b) + τ.(a k c) ⊲ M} ⊎ X while outputting a contains b and c…
Figure 13
Figure 13. Figure 13: The LTS of processes. The meta-variables are a ∈ N , µ ∈ Act, and α ∈ Actτ . The prefix a.p represents a blocked process, which waits to perform the input a, i.e. to interact with the atom a, and then becomes p; and atoms a , b , . . . represent output messages. We wi…
Figure 14
Figure 14. Figure 14: A typeclass for LTSs where a structural congruence exists over states. H.1 Structural equivalence and its properties To manipulate the syntax of processes we use a standard structural congru￾ence denoted ≡, stating that ACCS is a commutative monoid with identity 0 wit…
Figure 15
Figure 15. Figure 15: Rules to define structural congruence on ACCS. Lemma 53. For every p ∈ ACCS, 1. for every a ∈ N . p a −→ p ′ implies p ≡ p ′ k a , 2. there exists p ′ such that p ≡ p ′ k ΠM , and p ′ performs no output action. This lemma and Lemma 52 essentially hold, because, as alr…
Figure 16
Figure 16. Figure 16: Functions to generate clients. H.2 Client generators and their properties This subsection is devoted to the study of the semantic properties of the clients produced by the function g. In general these are the properties sufficient to obtain our completeness result. Le…
Figure 17
Figure 17. Figure 17: Typeclasses to formalise LTSs. J.4 Typeclasses for LTS Our basic typeclasses are Lts ≥ LtsEq ≥ LtsOba, where LtsOba is a super-class of both LtsObaFB and LtsObaFW. The class LtsObaFB represents output-buffered agents with feedback, while LtsObaFW represents output-buf…
Figure 7
Figure 7. Figure 7: Rules to define inductively the predicate [PITH_FULL_IMAGE:figures/full_fig_p087_7.png]

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

160 extracted references · 54 canonical work pages

  1. [1]

    Aceto, L., Achilleos, A., Francalanza, A., Ing´ olfsd´ ot tir, A., Lehtinen, K.: Adventures in monitorability: from branching to linear time and back again. Proc. ACM Program. Lang. 3(POPL), 52:1–52:29 (2019). https://doi.org/10.1145/3290365, https://doi.org/10.1145/3290365

    doi:10.1145/3290365 2019

  2. [2]

    Aceto, L., Hennessy, M.: Termination, Deadlock, and Dive rgence. J. ACM 39(1), 147–187 (1992). https://doi.org/10.1145/147508.147527, https://doi.org/10.1145/147508.147527

    arXiv 1992

  3. [3]

    In: Sch¨ urmann, C

    Affeldt, R., Kobayashi, N.: A Coq Library for Verification o f Concurrent Pro- grams. In: Sch¨ urmann, C. (ed.) Proceedings of the Fourth In ternational Work- shop on Logical Frameworks and Meta-Languages, LFM@IJCAR 2 004. Cork, Ire- land, July 5, 2004. Electronic Notes in Theoretical Compute r Science, vol. 199, pp. 17–32. Elsevier (2004). https://doi.org/...

    work page doi:10.1016/j.entcs.2007.11.010 2004

  4. [4]

    In: Montanari, U., Sassone, V

    Amadio, R.M., Castellani, I., Sangiorgi, D.: On Bisimula tions for the Asynchronous pi-calculus. In: Montanari, U., Sassone, V. (eds.) Proceed ings CONCUR 96, Pisa. Lecture Notes in Computer Science, vol. 1119, pp. 147–162. S pringer Verlag (1996)

    1996

  5. [5]

    Theoretical Computer Science 195, 291–324 (1998)

    Amadio, R.M., Castellani, I., Sangiorgi, D.: On Bisimula tions for the Asynchronous pi-calculus. Theoretical Computer Science 195, 291–324 (1998)

    1998

  6. [6]

    Master’s thesis, Massachusetts Institute of Technology (J un 2017)

    Athalye, A.: CoqIOA: A Formalization of IO Automata in the Coq Proof Assistant. Master’s thesis, Massachusetts Institute of Technology (J un 2017)

    2017

  7. [7]

    Aubert, C., Varacca, D.: Processes against tests: On defin ing con- textual equivalences. J. Log. Algebraic Methods Program. 129, 100799 (2022). https://doi.org/10.1016/J.JLAMP.2022.100799, https://doi.org/10.1016/j.jlamp.2022.100799

    arXiv 2022

  8. [8]

    In: Bodei, C., Ferrari, G., Priam i, C

    Baldan, P., Bonchi, F., Gadducci, F., Monreale, G.V.: Asy nchronous Traces and Open Petri Nets. In: Bodei, C., Ferrari, G., Priam i, C. (eds.) Programming Languages with Applications to Biology and Secu- rity - Essays Dedicated to Pierpaolo Degano on the Occasion o f His 65th Birthday. Lecture Notes in Computer Science, vol. 9465 , pp. 86–

Show all 160 references
  1. [9]

    In: Kutsia, T., Schreiner, W., Fern ´ andez, M

    Barbanera, F., de’Liguoro, U.: Two notions of sub-behavi our for session-based client/server systems. In: Kutsia, T., Schreiner, W., Fern ´ andez, M. (eds.) Pro- ceedings of the 12th International ACM SIGPLAN Conference o n Principles and Practice of Declarative Programming, J...

    2010

  2. [10]

    College Pub- lications (2022), https://www.collegepublications.co.uk/logic/mlf/?00035, chapter 11

    Barendregt, H., Manzonetto, G.: A Lambda Calculus Satel lite. College Pub- lications (2022), https://www.collegepublications.co.uk/logic/mlf/?00035, chapter 11

    2022

  3. [11]

    Acta Infor- matica 59(1), 125–162 (2022)

    Baxter, J., Ribeiro, P., Cavalcanti, A.: Sound reasonin g in tock-CSP. Acta Infor- matica 59(1), 125–162 (2022). https://doi.org/10.1007/s00236-020-00394-3 , https://doi.org/10.1007/s00236-020-00394-3

    2022 doi

  4. [12]

    Bernardi, G.: Behavioural equivalences for Web service s. Ph.D. thesis, Trinity Col- lege Dublin (2013), http://www.tara.tcd.ie/handle/2262/77595

    2013

  5. [13]

    https://doi.org/10.5281/zenodo.14617145, https://doi.org/10.5281/zenodo.10.5281/zenodo.14617145 26

    Bernardi, G., Castellani, I., Laforgue, P., Stefanesco , L.: Artifact for constructive characterisations of the must-preorder f or asyn- chrony (jan 2025). https://doi.org/10.5281/zenodo.14617145, https://doi.org/10.5281/zenodo.10.5281/zenodo.14617145 26

    2025 doi

  6. [14]

    Bernardi, G., Hennessy, M.: Mutually Testing Processes . Log. Meth- ods Comput. Sci. 11(2) (2015). https://doi.org/10.2168/LMCS-11(2:1)2015, https://doi.org/10.2168/LMCS-11(2:1)2015

    2015 doi

  7. [15]

    Bernardi, G., Hennessy, M.: Using higher-order con- tracts to model session types. Log. Methods Comput. Sci. 12(2) (2016). https://doi.org/10.2168/LMCS-12(2:10)2016, https://doi.org/10.2168/LMCS-12(2:10)2016

    2016 doi

  8. [16]

    Bernardi, G.T., Hennessy, M.: Modelling session types u s- ing contracts. Math. Struct. Comput. Sci. 26(3), 510– 560 (2016). https://doi.org/10.1017/S0960129514000243, https://doi.org/10.1017/S0960129514000243

    2016 doi

  9. [17]

    Berry, G., Boudol, G.: The Chemical Abstract Machine. Th eor. Comput. Sci. 96(1), 217–248 (1992). https://doi.org/10.1016/0304-3975(92)90185-I , https://doi.org/10.1016/0304-3975(92)90185-I

    1992 doi

  10. [18]

    In: Dowek, G

    Bizjak, A., Birkedal, L., Miculan, M.: A model of countab le nondeterminism in guarded type theory. In: Dowek, G. (ed.) Rewriting and Typed Lambda Calculi. pp. 108–123. Springer International Publishing, Cham (201 4)

  11. [19]

    In: Shan, C

    Bonchi, F., Caltais, G., Pous, D., Silva, A.: Brzozowski ’s and Up-To Algo- rithms for Must Testing. In: Shan, C. (ed.) Programming Lang uages and Sys- tems - 11th Asian Symposium, APLAS 2013, Melbourne, VIC, Aus tralia, De- cember 9-11, 2013. Proceedings. Lecture Notes in Com...

    2013 doi

  12. [20]

    Bonchi, F., Sokolova, A., Vignudelli, V.: The Theory of T races for Sys- tems with Nondeterminism, Probability, and Termination. L og. Methods Comput. Sci. 18(2) (2022). https://doi.org/10.46298/LMCS-18(2:21)2022, https://doi.org/10.46298/lmcs-18(2:21)2022

    2022 doi

  13. [21]

    Boreale, M., Gadducci, F.: Processes as formal power ser ies: A coinductive approach to denotational semantics. Theor. C om- put. Sci. (2006). https://doi.org/10.1016/j.tcs.2006.05.030, https://doi.org/10.1016/j.tcs.2006.05.030

    2006 doi

  14. [22]

    Boreale, M., Nicola, R.D.: Testing Equivalence for Mobi le Processes. Inf. Comput. 120(2), 279–303 (1995). https://doi.org/10.1006/inco.1995.1114, https://doi.org/10.1006/inco.1995.1114

    1995

  15. [23]

    Boreale, M., Nicola, R.D., Pugliese, R.: Trace and Testi ng Equivalence on Asynchronous Processes. Inf. Comput. 172(2), 139–164 (2002). https://doi.org/10.1006/inco.2001.3080, https://doi.org/10.1006/inco.2001.3080

    2002

  16. [24]

    Research Re port RR-1702, INRIA (1992), https://hal.inria.fr/inria-00076939

    Boudol, G.: Asynchrony and the Pi-calculus. Research Re port RR-1702, INRIA (1992), https://hal.inria.fr/inria-00076939

    1992

  17. [25]

    Boudol, G.: The pi-Calculus in Direct Style. High. Order Symb. Com- put. 11(2), 177–208 (1998). https://doi.org/10.1023/A:1010064516533, https://doi.org/10.1023/A:1010064516533

    1998 doi

  18. [26]

    In: Kirchner, H

    Boudol, G., Lavatelli, C.: Full Abstraction for Lambda C alculus with Re- sources and Convergence Testing. In: Kirchner, H. (ed.) Tre es in Algebra and Programming - CAAP’96, 21st International Colloquium, Lin k¨ oping, Sweden, April, 22-24, 1996, Proceedings. Lecture Notes in...

    1996 doi

  19. [27]

    In: FOSSACS (2021) 27

    Bravetti, M., Lange, J., Zavattaro, G.: Fair Refinement f or Asynchronous Session Types. In: FOSSACS (2021) 27

    2021

  20. [28]

    In: 36th Annual ACM/IEEE Symposium on L ogic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 20 21

    Brede, N., Herbelin, H.: On the logical structure of choi ce and bar in- duction principles. In: 36th Annual ACM/IEEE Symposium on L ogic in Computer Science, LICS 2021, Rome, Italy, June 29 - July 2, 20 21. pp. 1–13. IEEE (2021). https://doi.org/10.1109/LICS52264.2021.9470523...

    2021

  21. [29]

    In: Kesner, D., Pientka, B

    Breuvart, F., Manzonetto, G., Polonsky, A., Ruoppolo, D .: New Results on Morris’s Observational Theory: The Benefits of Separating t he Inseparable. In: Kesner, D., Pientka, B. (eds.) 1st International Conferenc e on Formal Structures for Computation and Deduction, FSCD 2016, ...

    2016 doi

  22. [30]

    Breuvart, F., Manzonetto, G., Ruoppolo, D.: Relational Graph Models at Work. Log. Methods Comput. Sci. 14(3) (2018). https://doi.org/10.23638/LMCS-14(3:2)2018, https://doi.org/10.23638/LMCS-14(3:2)2018

    2018 doi

  23. [31]

    In: D ´ ı az, J

    Brookes, S.D.: On the Relationship of CCS and CSP. In: D ´ ı az, J. (ed.) Automata, Languages and Programming, 10th Colloquiu m, Barcelona, Spain, July 18-22, 1983, Proceedings. Lecture Notes in Comp uter Science, vol. 154, pp. 83–96. Springer (1983). https://doi.org/10.1007/B...

    1983 doi

  24. [32]

    Brookes, S.D.: Deconstructing CCS and CSP Asynchronous Communication, Fairness, and Full Abstraction (2016), http://www.cs.cmu.edu/afs/cs/Web/People/brookes/papers/mfps16paper.pdf

    2016

  25. [33]

    Brookes, S.D., Hoare, C.A.R., Roscoe, A.W.: A Theory of C om- municating Sequential Processes. J. ACM 31(3), 560–599 (1984). https://doi.org/10.1145/828.833, https://doi.org/10.1145/828.833

    1984 doi

  26. [34]

    Master thesis, University of Malta (2019)

    Caruana, C.: Compositional Reasoning about Actor Based Systems. Master thesis, University of Malta (2019)

    2019

  27. [35]

    In: Porto, A., L´ opez-Fraguas, F.J

    Castagna, G., Dezani-Ciancaglini, M., Giachino, E., Pa dovani, L.: Founda- tions of session types. In: Porto, A., L´ opez-Fraguas, F.J. (eds.) Proceed- ings of the 11th International ACM SIGPLAN Conference on Pri nciples and Practice of Declarative Programming, September 7-9, ...

    2009

  28. [36]

    ACM Trans

    Castagna, G., Gesbert, N., Padovani, L.: A theory of con- tracts for Web services. ACM Trans. Program. Lang. Syst. 31(5), 19:1–19:61 (2009). https://doi.org/10.1145/1538917.1538920, https://doi.org/10.1145/1538917.1538920

    2009

  29. [37]

    In: Palmigiano, A., Sadrzadeh, M

    Castellan, S., Clairambault, P., Winskel, G.: The Mays a nd Musts of Concurrent Strategies. In: Palmigiano, A., Sadrzadeh, M . (eds.) Samson Abramsky on Logic and Structure in Computer Sci- ence and Beyond. pp. 327–361. Springer International Publi sh- ing, Cham (2023). https:...

    2023 doi

  30. [38]

    In: Arvind, V., Ramanujam, R

    Castellani, I., Hennessy, M.: Testing Theories for Asyn chronous Languages. In: Arvind, V., Ramanujam, R. (eds.) Foundations of Softwar e Technology and Theoretical Computer Science, 18th Conference, Chenna i, India, Decem- ber 17-19, 1998, Proceedings. Lecture Notes in Comput...

    1998

  31. [39]

    Cerone, A., Hennessy, M.: Process Behaviour: Formulae v s. Tests. Tech. rep., Trin- ity College Dublin, School of Computer Science and Statisti cs (2010)

    2010

  32. [40]

    CONCLUSION pp. 90–101. Springer (1998). https://doi.org/10.1007/978-3-540-49382-2_9 , https://doi.org/10.1007/978-3-540-49382-2_9

    1998 doi

  33. [41]

    In: Sifakis, J

    Cleaveland, R., Hennessy, M.: Testing Equivalence as a B isimulation Equivalence. In: Sifakis, J. (ed.) Automatic Verification M ethods for Fi- nite State Systems, International Workshop, Grenoble, Fra nce, June 12- 14, 1989, Proceedings. Lecture Notes in Computer Science, v ol...

    1989 doi

  34. [42]

    In: LICS (1991)

    Cleaveland, R., Zwarico, A.E.: A Theory of Testing for Re al-Time. In: LICS (1991)

    1991

  35. [43]

    De Nicola, R., Hennessy, M.: Testing Equivalences for Pr ocesses. Theor. Com- put. Sci. 34, 83–133 (1984). https://doi.org/10.1016/0304-3975(84)90113-0 , https://doi.org/10.1016/0304-3975(84)90113-0

    1984 doi

  36. [44]

    IEEE Transactions on Software Enginee ring 24(5), 315–330 (1998)

    De Nicola, R., Ferrari, G., Pugliese, R.: Klaim: a kernel language for agents inter- action and mobility. IEEE Transactions on Software Enginee ring 24(5), 315–330 (1998). https://doi.org/10.1109/32.685256

    1998 doi

  37. [45]

    De Nicola, R., Pugliese, R.: Linda-based applicative an d im- perative process algebras. Theor. Comput. Sci. 238(1-2), 389– 437 (2000). https://doi.org/10.1016/S0304-3975(99)00339-4 , https://doi.org/10.1016/S0304-3975(99)00339-4

    2000 doi

  38. [46]

    De Nicola, R., Melgratti, H.C.: Multiparty testing preo rders. Log. Meth- ods Comput. Sci. 19(1) (2023). https://doi.org/10.46298/lmcs-19(1:1)2023, https://doi.org/10.46298/lmcs-19(1:1)2023

    2023 doi

  39. [47]

    Oxford logic gui des, Clarendon Press (2000), https://books.google.fr/books?id=JVFzknbGBVAC

    Dummett, M.: Elements of Intuitionism. Oxford logic gui des, Clarendon Press (2000), https://books.google.fr/books?id=JVFzknbGBVAC

    2000

  40. [48]

    Dreyer, D., Neis, G., Birkedal, L.: The impact of higher- order state and control effects on local relational reasoning. J. Funct. Program. 22(4-5), 477–528 (2012). https://doi.org/10.1017/S095679681200024X, https://doi.org/10.1017/S095679681200024X

    2012 doi

  41. [49]

    Francalanza, A.: A theory of monitors. Inf. Comput. 281, 104704 (2021). https://doi.org/10.1016/j.ic.2021.104704, https://doi.org/10.1016/j.ic.2021.104704

    2021

  42. [50]

    In: Barthe, G., Dybjer, P., Pinto, L., Saraiva , J

    Fournet, C., Gonthier, G.: The join calculus: A language for distributed mobile programming. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva , J. (eds.) Applied Semantics. pp. 268–332. Springer Berlin Heidelberg, Berli n, Heidelberg (2002)

    2002

  43. [51]

    In: Dawar, A

    Frumin, D., Krebbers, R., Birkedal, L.: ReLoC: A Mechani sed Re- lational Logic for Fine-Grained Concurrency. In: Dawar, A. , Gr¨ adel, E. (eds.) Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2018, Oxford, UK, July 09-12 , 2018. pp. 442–4...

    2018

  44. [52]

    In: TYPES (1998), https://doi.org/10.1007/3-540-48167-2_7

    Fridlender, D.: An Interpretation of the Fan Theorem in T ype Theory. In: TYPES (1998), https://doi.org/10.1007/3-540-48167-2_7

    1998 doi

  45. [53]

    In: Kupferman, O., Soboc inski, P

    van Glabbeek, R.: Just Testing. In: Kupferman, O., Soboc inski, P. (eds.) Foun- dations of Software Science and Computation Structures - 26 th International Conference, FoSSaCS 2023, Held as Part of the European Joint Conferences 29

    2023

  46. [54]

    Acta Infor- matica 42(2-3), 191–225 (2005)

    Gay, S.J., Hole, M.: Subtyping for session types in the pi calculus. Acta Infor- matica 42(2-3), 191–225 (2005). https://doi.org/10.1007/s00236-005-0177-z , https://doi.org/10.1007/s00236-005-0177-z

    2005 doi

  47. [55]

    MIT Press s eries in the foundations of computing, MIT Press (1988)

    Hennessy, M.: Algebraic theory of processes. MIT Press s eries in the foundations of computing, MIT Press (1988)

    1988

  48. [56]

    Lecture Notes in Computer Science, v ol

    CONCLUSION on Theory and Practice of Software, ETAPS 2023, Paris, Franc e, April 22- 27, 2023, Proceedings. Lecture Notes in Computer Science, v ol. 13992, pp. 498–519. Springer (2023). https://doi.org/10.1007/978-3-031-30829-1_24 , https://doi.org/10.1007/978-3-031-30829-1_24

    2023 doi

  49. [57]

    Hennessy, M.: Acceptance Trees. J. ACM 32(4), 896–928 (1985). https://doi.org/10.1145/4221.4249, https://doi.org/10.1145/4221.4249

    1985

  50. [58]

    Cambridge Uni versity Press (2007)

    Hennessy, M.: A distributed Pi-calculus. Cambridge Uni versity Press (2007)

    2007

  51. [59]

    Hennessy, M.: A fully abstract denotational semantics for the pi-calculus. Theor. Comput. Sci. 278(1-2), 53– 89 (2002). https://doi.org/10.1016/S0304-3975(00)00331-5 , https://doi.org/10.1016/S0304-3975(00)00331-5

    2002 doi

  52. [60]

    Hennessy, M.: The security pi-calculus and non-interfe rence. J. Log. Alge- braic Methods Program. (2005). https://doi.org/10.1016/j.jlap.2004.01.003, https://doi.org/10.1016/j.jlap.2004.01.003

    2005 doi

  53. [61]

    resource ac cess in the asynchronous pi-calculus

    Hennessy, M., Riely, J.: Information flow vs. resource ac cess in the asynchronous pi-calculus. ACM Trans. Program. Lang. Sy st. 24(5), 566–591 (2002). https://doi.org/10.1145/570886.570890, https://doi.org/10.1145/570886.570890

    2002

  54. [62]

    Formal Aspects Comput

    Hennessy, M., Ing´ olfsd´ ottir, A.: Communicating Proc esses with Value- passing and Assignments. Formal Aspects Comput. 5(5), 432–466 (1993). https://doi.org/10.1007/BF01212486, https://doi.org/10.1007/BF01212486

    1993 doi

  55. [63]

    In: Dem binski, P

    Hennessy, M., Plotkin, G.D.: A Term Model for CCS. In: Dem binski, P. (ed.) Mathematical Foundations of Computer Science 1980 (M FCS’80), Pro- ceedings of the 9th Symposium, Rydzyna, Poland, September 1 -5, 1980. Lecture Notes in Computer Science, vol. 88, pp. 261–274. Spr ing...

    1980 doi

  56. [64]

    In: America, P

    Honda, K., Tokoro, M.: An Object Calculus for Asynchrono us Communi- cation. In: America, P. (ed.) ECOOP’91 European Conference on Object- Oriented Programming, Geneva, Switzerland, July 15-19, 19 91, Proceedings. Lecture Notes in Computer Science, vol. 512, pp. 133–147. Sp ri...

    1991 doi

  57. [65]

    In: Kupferman, O., Soboci nski, P

    Hirschkoff, D., Jaber, G., Prebet, E.: Deciding Contextu al Equivalence of ν- Calculus with Effectful Contexts. In: Kupferman, O., Soboci nski, P. (eds.) Foundations of Software Science and Computation Structure s - 26th Interna- tional Conference, FoSSaCS 2023, Held as Part of ...

    2023

  58. [66]

    Hoare, C.A.R.: Communicating Sequential Processes (Re print). Commun. ACM (1983)

    1983

  59. [67]

    Intrigila, B., Manzonetto, G., Polonsky, A.: Degrees of extensionality in the theory of B¨ ohm trees and Sall´ e’s conjecture. Log. Me thods Comput. Sci. 15(1) (2019). https://doi.org/10.23638/LMCS-15(1:6)2019, https://doi.org/10.23638/LMCS-15(1:6)2019 30

    2019 doi

  60. [68]

    In: Necula, G.C., Wadler, P

    Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchr onous Session Types. In: Necula, G.C., Wadler, P. (eds.) POPL. pp. 273–284. ACM Press , New York (2008)

    2008

  61. [69]

    Journal of ACM 63(1), 9:1–9:67 (2016)

    Honda, K., Yoshida, N., Carbone, M.: Multiparty Asynchr onous Session Types. Journal of ACM 63(1), 9:1–9:67 (2016)

    2016

  62. [70]

    In: Castagna, G., Gordon, A.D

    Krebbers, R., Timany, A., Birkedal, L.: Interactive pro ofs in higher-order concurrent separation logic. In: Castagna, G., Gordon, A.D . (eds.) Pro- ceedings of the 44th ACM SIGPLAN Symposium on Principles of P ro- gramming Languages, POPL 2017, Paris, France, January 18-2 0, ...

    2017

  63. [71]

    Studie s in logic and the foundations of mathematics, North-Holland Publishing Company (1965), https://books.google.fr/books?id=2EHVxQEACAAJ

    Kleene, S.C., Vesley, R.E.: The Foundations of Intuitio nistic Mathemat- ics: Especially in Relation to Recursive Functions. Studie s in logic and the foundations of mathematics, North-Holland Publishing Company (1965), https://books.google.fr/books?id=2EHVxQEACAAJ

    1965

  64. [72]

    In: LICS (2023)

    Koutavas, V., Tzevelekos, N.: Fully Abstract Normal For m Bisimulation for Call- by-Value PCF. In: LICS (2023)

    2023

  65. [73]

    In: Paterson, M

    Milner, R.: Functions as Processes. In: Paterson, M. (ed .) Automata, Languages and Programming, 17th International Colloquium, ICALP90, Warwick University, England, UK, July 16-20, 1990, Proceedings. Lecture Notes i n Computer Science, vol. 443, pp. 167–180. Springer (1990). ...

    1990 doi

  66. [74]

    Addison-Wesley (2002 ), http://research.microsoft.com/users/lamport/tla/book.html

    Lamport, L.: Specifying Systems, The TLA+ Language and T ools for Hardware and Software Engineers. Addison-Wesley (2002 ), http://research.microsoft.com/users/lamport/tla/book.html

    2002

  67. [75]

    In: Caires, L., Vasconcelos, V.T

    Laneve, C., Padovani, L.: The Must Preorder Revisited. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 - Concurrency Theory, 18th In- ternational Conference, CONCUR 2007, Lisbon, Portugal, Se ptember 3- 8, 2007, Proceedings. Lecture Notes in Computer Science, vo l. 4703, ...

    2007 doi

  68. [76]

    In: Ehrig , H., Kowalski, R.A., Levi, G., Montanari, U

    Nicola, R.D., Hennessy, M.: CCS without tau’s. In: Ehrig , H., Kowalski, R.A., Levi, G., Montanari, U. (eds.) TAPSOFT’87: Proceedin gs of the Inter- national Joint Conference on Theory and Practice of Softwar e Development, Pisa, Italy, March 23-27, 1987, Volume 1: Advanced Se...

    1987 doi

  69. [77]

    Cambridge University Press (1999)

    Milner, R.: Communicating and Mobile Systems - the Pi-Ca lculus. Cambridge University Press (1999)

    1999

  70. [78]

    Morris, J.H.: Lambda-calculus models of programming la n- guages. Ph.D. thesis, Massachusetts Institute of Technolo gy (1969), https://dspace.mit.edu/handle/1721.1/64850

    1969

  71. [79]

    In: Bojanczyk, M., Merelli, E., W oodruff, D.P

    Prebet, E.: Functions and References in the Pi-Calculus : Full Abstrac- tion and Proof Techniques. In: Bojanczyk, M., Merelli, E., W oodruff, D.P. (eds.) 49th International Colloquium on Automata, Lan guages, 31

  72. [80]

    Mathematical Structures in Computer Science 13(5), 685–719 (2003)

    Palamidessi, C.: Comparing the Expressive Power of the S ynchronous and Asyn- chronous pi-calculi. Mathematical Structures in Computer Science 13(5), 685–719 (2003). https://doi.org/10.1017/S0960129503004043

    2003 doi

  73. [81]

    In: Grohe, M., Koski nen, E., Shankar, N

    Pous, D.: Coinduction All the Way Up. In: Grohe, M., Koski nen, E., Shankar, N. (eds.) Proceedings of the 31st Annual ACM/IEEE S ymposium on Logic in Computer Science, LICS ’16, New York, NY, USA, Jul y 5-8,

  74. [82]

    Ravara, A., Resende, P., Vasconcelos, V.T.: An Algebra o f Behavioural Types. Inf. Comput. 212, 64–91 (2012)

    2012

  75. [83]

    Rensink, A., Vogler, W.: Fair testing. Inf. Comput. 205(2), 125–198 (2007). https://doi.org/10.1016/j.ic.2006.06.002, https://doi.org/10.1016/j.ic.2006.06.002

    2007 doi

  76. [84]

    LIPIcs, vol

    CONCLUSION and Programming, ICALP 2022, July 4-8, 2022, Paris, France. LIPIcs, vol. 229, pp. 130:1–130:19. Schloss Dagstuhl - Leibniz-Zen trum f¨ ur In- formatik (2022). https://doi.org/10.4230/LIPIcs.ICALP.2022.130, https://doi.org/10.4230/LIPIcs.ICALP.2022.130

    2022 doi

  77. [85]

    Pugliese, R.: Semantic Theories for Asynchronous Langu ages. Ph.D. thesis, Uni- versit` a di Roma ”La Sapienza” (1996)

    1996

  78. [86]

    Rahli, V., Bickford, M., Cohen, L., Constable, R.L.: Bar Induction is Com- patible with Constructive Type Theory. J. ACM 66(2), 13:1–13:35 (2019). https://doi.org/10.1145/3305261, https://doi.org/10.1145/3305261

    2019 doi

  79. [87]

    Cam- bridge University Press (2001)

    Sangiorgi, D., Walker, D.: The Pi-Calculus - a Theory of M obile Processes. Cam- bridge University Press (2001)

    2001

  80. [88]

    In: Dardha, O., Rot, J

    Schmidt-Schauß, M., Sabel, D.: Correctly Implementing Synchronous Mes- sage Passing in the Pi-Calculus By Concurrent Haskell’s MVa rs. In: Dardha, O., Rot, J. (eds.) Proceedings Combined 27th Intern ational Work- shop on Expressiveness in Concurrency and 17th Workshop on S tru...

    2020 doi

  81. [89]

    Sabel, D., Schmidt-Schauß, M.: A call-by-need lambda ca lcu- lus with locally bottom-avoiding choice: context lemma and cor- rectness of transformations. Math. Struct. Comput. Sci. 18(3), 501–553 (2008). https://doi.org/10.1017/S0960129508006774, https://doi.org/10.1017/S09601...

    2008 doi

  82. [90]

    Cambridge Univer- sity Press (2011)

    Sangiorgi, D.: Introduction to Bisimulation and Coindu ction. Cambridge Univer- sity Press (2011)

    2011

  83. [91]

    In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia , F

    Sangiorgi, D.: Asynchronous pi-calculus at Work: The Ca ll-by-Need Strategy. In: Alvim, M.S., Chatzikokolakis, K., Olarte, C., Valencia , F. (eds.) The Art of Modelling Computational Systems: A Journey from Logic and C oncurrency to Security and Privacy - Essays Dedicated to C...

    2019 doi

  84. [92]

    Archive of Formal Proofs (November 2020), https://isa-afp.org/entries/CSP_RefTK.html, Formal proof development

    Taha, S., Wolff, B., Ye, L.: The hol-csp refinement toolkit . Archive of Formal Proofs (November 2020), https://isa-afp.org/entries/CSP_RefTK.html, Formal proof development

    2020

  85. [93]

    Tanti, E., Francalanza, A.: Towards Sound Refactoring i n Erlang (2015), https://api.semanticscholar.org/CorpusID:63046364

    2015

  86. [94]

    In: Sabel, D., Thiemann, P

    Schmidt-Schauß, M., Sabel, D., Dallmeyer, N.: Sequenti al and Paral- lel Improvements in a Concurrent Functional Programming La nguage. In: Sabel, D., Thiemann, P. (eds.) Proceedings of the 20th In terna- tional Symposium on Principles and Practice of Declarative Program- ming...

    2018

  87. [95]

    In: Ma zurkiewicz, A.W., Winkowski, J

    Selinger, P.: First-Order Axioms for Asynchrony. In: Ma zurkiewicz, A.W., Winkowski, J. (eds.) CONCUR ’97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 19 97, Pro- ceedings. Lecture Notes in Computer Science, vol. 1243, pp. 376–

  88. [97]

    Archive o f Formal Proofs (April 2019)

    Taha, S., Ye, L., Wolff, B.: HOL-CSP Version 2.0. Archive o f Formal Proofs (April 2019)

    2019

  89. [100]

    Thati, P.: A Theory of Testing for Asynchronous Concurre nt Systems. Ph.D. thesis, University of Illinois Urbana-Champaign, US A (2003), https://hdl.handle.net/2142/81630

    2003

  90. [101]

    In: Giacobazz i, R., Cousot, R

    Turon, A.J., Thamsborg, J., Ahmed, A., Birkedal, L., Dre yer, D.: Logi- cal Relations for Fine-Grained Concurrency. In: Giacobazz i, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Prin ciples of Programming Languages, POPL ’13, Rome, Italy - January 23 - 25,

  91. [102]

    https://doi.org/10.1007/978-3-319-25527-9_8 , https://doi.org/10.1007/978-3-319-25527-9_8

    Springer (2015). https://doi.org/10.1007/978-3-319-25527-9_8 , https://doi.org/10.1007/978-3-319-25527-9_8

    2015 doi

  92. [103]

    The more sophisticated the languages, th e more intri- cate and larger the proofs

    as well as in languages supporting shared memory concurrency [95], and mutable references [46]. The more sophisticated the languages, th e more intri- cate and larger the proofs. The need for mechanisation became th us apparent, in particular to prove that complex logical rela...

  93. [104]

    if p ⇓ s and p τ − →p′ then p′ ⇓ s,

  94. [105]

    p ⇓ µ.s and p µ − →p′ imply p ⇓ s

    for every µ ∈ Act. p ⇓ µ.s and p µ − →p′ imply p ⇓ s. Lemma 10. For every s ∈ Act⋆ and p ∈ ACCS, if p ⇓ s then | {q | p s =⇒ q} | ∈ N. The hypothesis of convergence in Lemma 10 is necessary. This is witn essed by the process p = recx.(x ‖ a), which realises an ever lasting add...

  95. [106]

    p1 /llceilr2 τ − →ˆp /llceilˆr, and

  96. [107]

    We prove p2 musti r1 by applying rule [ind-rule]

    For every p′, r′ such that p1 /llceilr2 τ − →p′ /llceilr′ we have that p′ musti r′. We prove p2 musti r1 by applying rule [ind-rule]. In turn this requires us to show that (i) p2 /llceilr1 τ − →, and that (ii) for each p′ and r′ such that p2 /llceilr1 τ − →p′ /llceilr′, we hav...

  97. [108]

    p1 ⊲ M1 τ − →fw p3 ⊲ M3, or

  98. [109]

    FOR W ARDERS We proceed by case analysis on the last rule used to derive the trans ition p1 ⊲ M 1 a − →fw p2 ⊲ M 2

    p1 ⊲ M1 .= p3 ⊲ M3 43 C. FOR W ARDERS We proceed by case analysis on the last rule used to derive the trans ition p1 ⊲ M 1 a − →fw p2 ⊲ M 2. This transition can either be derived by the rule [L- Mout] or the rule [L-Proc]. We first consider the case where the transition has bee...

  99. [110]

    p τ /arrownot− →and p s =⇒ p′ implies p′ τ /arrownot− →. 47 D. COMPLETENESS

  100. [111]

    Lemma 24

    p τ /arrownot− →and p s =⇒ p′ implies I(p) = I(p′). Lemma 24. For every s ∈ Act⋆, tc (s) τ − →. The Backward-output-determinacy axiom is used in the proof of the next lemma. Lemma 25. For every s ∈ Act⋆, if tc (s) µ − →r then either (a) good(r), or (b) s = s1. µ.s2 for some s1...

  101. [112]

    We prove the first property as we did in the base case, and we apply L emma 27 to prove the second property

    for every p′ such that p µ =⇒ p′, p′ ⇓ s′. We prove the first property as we did in the base case, and we apply L emma 27 to prove the second property. Lemma 29. Let LA ∈ Fwd. For every p ∈ A, s1 ∈ N ⋆ and s3 ∈ Act⋆ we have that

  102. [113]

    for every µ ∈ Act, if p ⇓ s1.µ.s3 and p µ − →q then q ⇓ s1.s3,

  103. [114]

    a.s3 then p ⇓ s1.s2.s3

    for every a.s2 ∈ N ⋆ if p ⇓ s1.a.s2. a.s3 then p ⇓ s1.s2.s3. Lemma 30. For every LTS LA and every p ∈ A, p ↓i implies p musti tc(ε). Proof. Rule induction on the derivation of p ↓i. Lemma 31. For every LA ∈ Fwd, every p ∈ A, and s ∈ Act⋆, if p ⇓ s then p musti tc(s). 48 D. COM...

  104. [115]

    there exist a ∈ N , s1, s2 and s3 with s = s1.a.s2.a.s3 and r ≃ tc(s1.s2.s3). If good(r) then we conclude via rule [axiom]; otherwise Lemma 29(2) and the hypothesis that p ⇓ s imply p ⇓ s1.s2.s3, thus prove p musti r via the inductive hypothesis of the complete induction on s....

  105. [116]

    a τ -transition performed by the client such that ta(a.s, O) τ − →r, or

  106. [117]

    In the first case Table 1(4) implies good(r), and hence we obtain p′ musti r via rule [axiom]

    an interaction between the server p and the client ta(a.s, O). In the first case Table 1(4) implies good(r), and hence we obtain p′ musti r via rule [axiom]. In the second case there exists an action µ such that p µ − →p′ and ta(a.s, O) µ − →r Table 1(5) implies µ is a and r = ...

  107. [118]

    p /llceilta(s, O(p) \ O) − →, and

  108. [119]

    To prove (1), we show that an interaction between the server p and the test ta(s, O(p) \ O) exists

    for each p′, r such that p /llceilta(s, O(p) \ O) τ − →p′ /llceilr, p′ musti r holds. To prove (1), we show that an interaction between the server p and the test ta(s, O(p) \ O) exists. As a ∈ O(p), we have that p a − →. Then a ∈ O(p) \ O together with (3) ensure that ta(s, O(...

  109. [120]

    a τ -transition performed by the server p such that p τ − →p′, or

  110. [121]

    12 Recall that the definition of ↓i is in Equation (int-preds) 52 E

    an interaction between the server p and the client ta(ε, ⋃ Afw(p, s) \ O). 12 Recall that the definition of ↓i is in Equation (int-preds) 52 E. SOUNDNESS In the first case we apply the first part of the inductive hypothesis to prove that p′ musti ta(ε, ⋃ Afw(p′, s) \ O), and we c...

  111. [123]

    Lemma 37

    X ↓i, X µ =⇒ X ′ and q µ − →q′ imply X ′≼ set cnv q′. Lemma 37. Let LA, LB ∈ Fwd. For every X, X ′ ∈ P +(A) and q ∈ B, such that X≼ set acc q, then

  112. [125]

    The main technical work for the proof of soundness is carried out b y the next lemma

    if X ↓i then for every µ ∈ Act, every q′ and X ′ such that q µ − → q′ and X µ =⇒ X ′ we have X ′≼ set acc q′. The main technical work for the proof of soundness is carried out b y the next lemma. Lemma 38. Let LA, LB ∈ Fwd and LC ∈ Fdb. For every set of servers X ∈ P +(A), ser...

  113. [127]

    if X ↓i and q µ − →q′ then for every set X µ =⇒ X ′ we have that X ′≼ set cnv q′. Proof. We first prove part (1). Let us fix a trace s such that X ⇓ s. We must show q′ ⇓ s. An application of the hypothesis X≼ set cnv q ensures q ⇓ s. From the transition q τ − →q′ and the fact th...

  114. [128]

    The first requirement follows from the hypothesis X ↓i

    for any p′ such that p µ =⇒ p′ we have p′ ⇓ s. The first requirement follows from the hypothesis X ↓i. The second requirement follows from the transition p µ =⇒ p′, from the assumption X ′ ⇓ s, and the hypothesis that X µ =⇒ X ′, which ensures that p′ ∈ X ′ and thus by definitio...

  115. [130]

    for every µ ∈ Act, if X ↓i, then for every q µ − →q′ and set X µ =⇒ X ′ we have X ′≼ set acc q′. Proof. To prove part (1) fix a trace s ∈ Act⋆ such that X ⇓ s. We have to explain why Afw(X, s) ≪ A fw(q′, s). By unfolding the definitions, this amounts to showing that ∀O ∈ A fw(q′...

  116. [131]

    The cases that correspond to a reduction of the mailbox M are dealt with di- rectly using the coinductive hypothesis (CH), since the mailbox is qua ntified universally in (CH). In more detail, consider the case where the redu ction (10) is of the form: a ‖ (τ.b + τ.c) ⊲ M b − →...

  117. [132]

    If (10) corresponds to a transition of the process, it must be t hat µ = a and q = τ.b + τ.c ⊲ M . In that case, the set X ′ of processes reached from {τ.(a ‖ b) + τ.(a ‖ c) ⊲ M } ⊎ X while outputting a contains b and c, so that X ′≼ co q follows from the general fact that {p,...

  118. [133]

    p s =⇒ q iff p nf(s) =⇒ · ≃ q, and if the first trace does not pass through a successful state then the normal form does not either,

  119. [134]

    We thereby obtain two other characterisations of the contextual preorder⊏ ∼must: Theorem 1 and Lemma 49 ensure that the preorders ⊏ ∼must and≼ NF AS coincide

    Afw(p, s) = Afw(p, nf(s)). We thereby obtain two other characterisations of the contextual preorder⊏ ∼must: Theorem 1 and Lemma 49 ensure that the preorders ⊏ ∼must and≼ NF AS coincide. Corollary 4. For every LA, LB ∈ Fdb, every p ∈ A and q ∈ B, p⊏ ∼must q iff FW(p)≼ NF AS FW(q...

  120. [135]

    p1 τ − →p′ 1 and q = p′ 1 ‖ p2,

  121. [136]

    p2 τ − →p′ 2 and q = p1 ‖ p′ 2,

  122. [137]

    p1 a − →p′ 1 and p2 a − →p′ 2 and q = p′ 1 ‖ p′ 2,

  123. [138]

    In the third case the number of possible output actions a is finite thanks to Lemma 50, and so is the number of reducts p′ 1 and p′ 2, so the set of term p′ 1 ‖ p′ 2 is decidable

    p1 a − →p′ 1 and p2 a − →p′ 2 and q = p′ 1 ‖ p′ 2. In the third case the number of possible output actions a is finite thanks to Lemma 50, and so is the number of reducts p′ 1 and p′ 2, so the set of term p′ 1 ‖ p′ 2 is decidable. The same argument works for the fourth case. Th...

  124. [139]

    p a − →p′ implies p ≡ p′ ‖ a ,

    for every a ∈ N . p a − →p′ implies p ≡ p′ ‖ a ,

  125. [140]

    This lemma and Lemma 52 essentially hold, because, as already pointed out in Section 2, the syntax enforces outputs to have no continuation

    there exists p′ such that p ≡ p′ ‖ ΠM , and p′ performs no output action. This lemma and Lemma 52 essentially hold, because, as already pointed out in Section 2, the syntax enforces outputs to have no continuation. The following lemma states a fundamental fact ([58, Lemma 2.13...

  126. [141]

    if p µ − →fw p′ and q µ − →q′ then p ‖ q τ − →p′ ‖ q′ or p ‖ q ≡ p′ ‖ q′

    for every µ ∈ Act. if p µ − →fw p′ and q µ − →q′ then p ‖ q τ − →p′ ‖ q′ or p ‖ q ≡ p′ ‖ q′

  127. [142]

    if p s =⇒fw p′ and q s =⇒ q′ then p ‖ q ε =⇒ · ≡ p′ ‖ q′

    for every s ∈ Act⋆. if p s =⇒fw p′ and q s =⇒ q′ then p ‖ q ε =⇒ · ≡ p′ ‖ q′. Obviously, for every p, q ∈ A and output a ∈ N we have p τ − →fw q if and only if p τ − →q (12) p ε =⇒fw q if and only if p ε =⇒ q (13) p a − →fw q if and only if p a − →q (14) together with the expe...

  128. [143]

    The equalities s = ν.s′ and s′ = s′ 1

    Since ν is an input we have s1 ∈ N ⋆. The equalities s = ν.s′ and s′ = s′ 1. µ .s′ 2 imply that s = s1 µ s2. The required o ≡ Π s1 ‖ g(s′ 2, q) follows from o′ ≡ Π s′ 1 ‖ g(s′ 2, q) and Equation (24). Now we proceed as follows, g(s, q) = ν ‖ g(s′, q) By Equation (20) ≡ ν ‖ (Π ...

  129. [144]

    If ν is an output, then g(ν.s′, q) = ν.(g(s′, q)) + τ

    We have p ≡ ν ‖ ˆp ≡ ν ‖ g(s′ 1.s′ 2, q) ≡ g(ν.s′ 1.s′ 2, q) as required. If ν is an output, then g(ν.s′, q) = ν.(g(s′, q)) + τ. 1. We prove part (b) and choose s1 = ε, s2 = s′. The hypothesis g(ν.s′, q) µ − →p implies that µ = ν and p ≡ g(s′, q) ≡ g(ε.s′, q) as required. 70 H...

  130. [145]

    We also have s′ = s′ 1.µ.s′ 2

    Since s′ 1.µ.s′ 2 ∈ N ⋆, we have s1.µ.s2 ∈ N ⋆. We also have s′ = s′ 1.µ.s′ 2. µ.s′ 3 By inductive hypothesis ν.s′ = ν.s′ 1.µ.s′ 2. µ.s′ 3 s = ν.s′ 1.µ.s′ 2. µ.s′ 3 Because s = ν.s′ s = s1.µ.s2. µ.s3 By definition It remains to prove that o ≡ g(s1.s2.s3, q). This is a consequen...

  131. [146]

    R(g(s, q)) = s ∪ R(q). Proof. By induction on s. In the base case ε ∈ N ⋆, and g(ε, q) = q, thus q τ /arrownot− →. The last two points follow from this equality and from ε containing no actions. In the inductive case s = µ.s′. The hypothesis g(µ.s′, q) τ /arrownot− →and the de...

  132. [147]

    for every I(q) ∩ s′ = ∅,

  133. [148]

    From R(g(s′, q)) = s′ ∪ R(q) we obtain R(g(s, q)) = s ∪ R(q)

    for every R(g(s′, q)) = s′ ∪ R(q) Since µ ‖ g(s′, q) τ /arrownot− →rule [Com] cannot be applied, thus q µ /arrownot− →, and so I(q) ∩ s = ∅. From R(g(s′, q)) = s′ ∪ R(q) we obtain R(g(s, q)) = s ∪ R(q). Lemma 70. For every µ ∈ Act, s and p, g(µ.s, p) µ − →g(s, p). Proof. We pr...

  134. [149]

    We prove (b)

    with s′ 1 ∈ N ∗. We prove (b). We choose b = µ, s1 = ε, s2 = s′ 1, s3 = s′

  135. [150]

    µ.s′ 2 = ε.µ.s′ 1

    We show the first requirement by s = µ.s′ = µ.s′ 1. µ.s′ 2 = ε.µ.s′ 1. µ.s′ 2 = s1.b.s2. b.s3. The second requirement is q = 0 ‖ q′ ≡ c(s′ 1.s′

  136. [151]

    We now consider the case (ii)

    = c(s1.s2.s3). We now consider the case (ii). The inductive hypothesis tells us that e ither:

  137. [152]

    ι.s′ 3 and q′ ≡ c(s′ 1.s′ 2.s′ 3)

    there exist ι, s′ 1, s′ 2 and s′ 3 with s′ 1.ι.s′ 2 ∈ N ∗ such that s′ = s′ 1.ι.s′ 2. ι.s′ 3 and q′ ≡ c(s′ 1.s′ 2.s′ 3). If (1) is true then we prove a with q = µ ‖ q′ and µ ‖ q′ and good(q′). If (2) is true then we prove (b). We choose b = ι, s1 = µ.s′ 1, s2 = s′ 2, s3 = s′

  138. [153]

    ι.s′ 3 = s1.b.s2

    We show the first requirement with s = µ.s′ = µ.s′ 1.ι.s′ 2. ι.s′ 3 = s1.b.s2. b.s3. The second requirement is q = µ ‖ q′ ≡ µ ‖ c(s′ 1.s′ 2.s′

  139. [154]

    If µ is an output then c(µ.s′) = µ.(cs′) + τ

    = c(s1.s2.s3). If µ is an output then c(µ.s′) = µ.(cs′) + τ. 1. The hypothesis c(µ.s′) τ − →q implies q = 1. We prove (a) with good(1). I Counter-example to existing completeness result In this section we recall the definition of the alternative preorder ≪ch by [38], and show t...

  140. [155]

    We illustrate the three auxiliary definitions using the process Pierre = b.(τ.Ω + c.d) introduced in Example 3

    for every R ∈ A(q, s) and every I ∈ IM (p, s) such that I ∩ R = ∅ there exists some O ∈ GA (p, s, I) such that O \ I ⊆ R. We illustrate the three auxiliary definitions using the process Pierre = b.(τ.Ω + c.d) introduced in Example 3. We may infer that Pierre { |b,c| } ↝ d (29) ...

  141. [156]

    I(Pierre) ∩ { |b, c| } ⁄= ∅,

  142. [157]

    Pierre a =⇒ p′ implies a = b, and

  143. [158]

    p − → q" := ( lts_step p τ q). 27 Notation

    There are two different states p′ such that Pierre b =⇒ p′, but the only one that can do the input c is p′ = τ.Ω + c.d. 75 J. HIGHLIGHTS OF THE COQ MECHANISATION This implies that the only way to infer Pierre { |b,c| } ↝ p′′ is via the derivation tree that proves Equation (29) ...

  144. [159]

    p ↓ if and only if p ↓i,

  145. [160]

    ps ≼ x1 q

    for every r we have that p must r if and only if p musti r. 1 Context `{ Label L }. 2 Context `{! Lts A L , ! FiniteLts A L }. 3 4 Lemma terminate_extensional_iff_terminate (p : A) : 5 terminate_extensional p <-> terminate p . 6 7 Inductive must_sts `{ Sts (A * B), good : B ->...

  146. [161]

    q τ − →q′ implies X≼ set cnv q′,

  147. [162]

    Lemma 37 Let LA, LB ∈ Fwd

    X ↓i, X µ =⇒ X ′ and q µ − →q′ imply X ′≼ set cnv q′. Lemma 37 Let LA, LB ∈ Fwd. For every X, X ′ ∈ P +(A) and q ∈ B, such that X≼ set acc q, then

  148. [163]

    q τ − →q′ implies X≼ set acc q′,

  149. [164]

    p ≼ 2 q" := ( bhv_lin_pre_cond2 p q ) ( at level 70). 12 13 Definition bhv_lin_pre `{@ Lts P L HL , @ Lts Q L HL } ( p : P) ( q : Q) := p ≼ 1 q /\ p ≼ 2 q. 14 15 Notation

    for every µ ∈ Act, if X ↓i, then for every q µ − →q′ and set X µ =⇒ X ′ we have X ′≼ set acc q′. 1 Lemma bhvx_preserved_by_tau 2 `{@ FiniteLts P L HL LtsP , @ FiniteLts Q L HL LtsQ } 3 (ps : gset P ) ( q q' : Q) : q − → q' -> ps ≼ x q -> ps ≼ x q' . 4 5 Lemma bhvx_preserved_by...

  150. [390]

    https://doi.org/10.1007/3-540-63141-0_26 , https://doi.org/10.1007/3-540-63141-0_26 32 A

    Springer (1997). https://doi.org/10.1007/3-540-63141-0_26 , https://doi.org/10.1007/3-540-63141-0_26 32 A. FURTHER RELATED WORKS

    1997 doi

  151. [2013]

    pp. 343–356. ACM (2013). https://doi.org/10.1145/2429069.2429111, https://doi.org/10.1145/2429069.2429111 A Further related works Contextual preorders in functional languages Morris preorder is actively studied in the pure λ-calculus [29,30,67,10], λ-calculus with references [...

    2013

  152. [2016]

    pp. 307–316. ACM (2016). https://doi.org/10.1145/2933575.2934564, https://doi.org/10.1145/2933575.2934564

    2016

Pith tools

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