1 Introduction↩︎

One of the reasons why people flock to cinemas to watch sequels and “rebooted” movies is that they know what they are getting into: they are familiar with the characters and the basic setup. Keeping with the cinematographic metaphor, we will cut to the chase and assume that the reader is already on board with the idea that the best assurance of the correctness of properties of a formal calculus is a machine-checked proof. In fact, this is becoming the norm in the semantics of programming languages; it is less established when concurrency is concerned, although the latter is of overwhelming importance in modern computing.

Enter the Concurrent Calculi Formalization Benchmark [@ConcBench] (CCFB), which provides a suite of problems designed to evaluate the formalization of concurrent and distributed language models, in particular process calculi. Following the methodology of the POPLMark challenge, CCFB aims to assess current mechanization techniques, identify optimal formalization patterns, and ideally drive improvements in proof assistant tooling. The CCFB framework structures this evaluation around three orthogonal challenges: the management of linear resources, the handling of scope extrusion, and the implementation of coinductive proof techniques. For the latter, the challenge is to prove the “context lemma” for strong barbed bisimilarity, namely that this notion of bisimilarity can be turned into a congruence by making it sensitive to substitution and parallel composition.

Induction is one of the great success stories of proof assistants: although systems differ in the details of their foundations and automation, inductive definitions and proofs by induction are supported in essentially comparable ways across the board. Coinduction has had a less uniform history; for a survey, we refer to [@HandPACoind]. The earliest systematic approach, due to Paulson, treats coinductive predicates as greatest fixed points of monotone operators, from which the corresponding coinduction principles are derived. A different tradition, familiar from Rocq/Coq, is based on guarded corecursion: coinductive objects are introduced by constructors, and recursive calls must occur under such constructors to ensure productivity. This discipline is often brittle in proof developments, especially when coinductive arguments are nested, combined with induction, or hidden behind auxiliary lemmas. Agda has explored several alternatives over time, from delays to sized types and observational presentations of codata to guarded type theories with the “later” modality [@Nakano00]. Similarly, Beluga has embraced sized types and copatterns [@ThibodeauCP16]. These developments are particularly relevant for mechanized concurrency, where bisimulations and up-to techniques routinely require coinductive proofs that are interleaved with substantial inductive reasoning about syntax, transitions, substitutions, and contexts.

The present paper is the conclusion of the Beluga “trilogy” of solutions to CCFB, initiated with [@ZackonSMP25] — featuring, among other contributions, a solution to the linearity challenge — and followed by [@Cecilia24] with the mechanization of the Harmony Lemma. As in any good sequel, we borrow from the latter paper the implementation of the syntax and the LTS-based operational semantics of the \(\pi\)-calculus, while crucially extending it with replication. After all, this is what makes behavioral equivalence interesting. And interesting it turns out to be, as there is a twist in this movie: the rule governing replication as proposed in [@ConcBench] is insufficient to establish the main result of the challenge. In fact, under this rule, structural congruence is not included in strong barbed similarity. This is problematic, because structural congruence is the baseline syntactic equivalence between processes and the context lemma relies crucially on this specific inclusion.

While this lapse is mildly embarrassing, given the singleton intersection between the authors of the Benchmark and of the present paper, it is once more a reaffirmation of the usefulness of mechanizations in proof assistants.

We will assume familiarity with the basic notions of the \(\pi\)-calculus as in the first chapters of [@SWBook], as well as a working knowledge of Beluga, both of its syntax and of its approach to proof checking. In particular we will only briefly touch upon the way Beluga handles coinduction via observations and refer the reader to [@ThibodeauCP16] for the theory and to [@MomiglianoPT19] for an application.

In the following, the statements of informal lemmas, theorems and proofs are hyperlinked via the accompanying cute icon to their formalization in the repository:

As a final note, we have cut one corner: we have concentrated on similarity, precongruence, etc., rather than bisimilarity and congruence. Extending the results to the symmetric case would only duplicate the code with no new insights and could be left to automation, perhaps a coding agent.

2 The \(\pi\)-Calculus and its Operational Semantics↩︎

To make the paper self-contained, we present the main definitions of the syntax and the labelled transition system (LTS) of the fragment of the \(\pi\)-calculus under study. For more details about the informal definitions, we refer the reader to [@SWBook].

2.1 Syntax↩︎

We follow the definitions of CCFB3 excluding sums and (mis)match, while we diverge from it by allowing the calculus to be name-passing rather than value-passing. That original separation of concerns is not a simplification in the HOAS approach, but just a quirk. \[P, Q \;\vcentcolon \vcentcolon = \;\boldsymbol{0} \;\mid \;x(y).P \;\mid \;\bar{x}y.P \;\mid \;(P \mid Q) \;\mid \;(\nu x) P \;\mid \;! P\] Recall that the input prefix \(x(y).P\) and the restriction \((\nu y) P\) both bind the name \(y\) in \(P\), while any other occurrence of names in a process is free. Accordingly, we write fn(\(P\)) and bn(\(P\)) for the sets of free and bound names occurring in a process.

Beluga is based on a two-level system, with the LF level for representing data and a computation level for reasoning about it via recursion and pattern matching. In the encoding, names are defined by

an LF type names without any constructor, together with a context schema that allows names to occur in other (open) LF objects. Since we define no other context schema, all the variables in open terms will have type names. Processes are LF objects, encoded using (weak) HOAS for input and restriction, as well known and detailed in [@Cecilia24]; their encoding is displayed in Fig. 1. Throughout the development, lowercase identifiers denote LF types, while those beginning with an uppercase letter denote computation-level data.

2.2 Operational Semantics↩︎

Actions include inputs \(x(y)\), free and bound outputs \(\bar{x}y\) and \(\bar{x}(y)\), and internal communications \(\tau\) . In inputs and bound outputs, the occurrences of the name \(y\) are bound, while all other name occurrences in actions are free; from this, we obtain the standard notions of free names, bound names and names occurring in an action \(\alpha\), respectively denoted as fn(\(\alpha\)), bn(\(\alpha\)) and n(\(\alpha\)).

Our LTS, displayed in Fig. 2, presents some differences from the one in CCFB3. First, and less importantly, we have adopted late instead of early semantics: not only can they be proven equivalent in terms of transitions, see [@Cecilia24] for the mechanization of this folk result, but they induce the same strong barbed similarity, as established by Lemma 4 below and the discussion that follows. Secondly, as we teased in the introduction, we add two replication rules for communication to the LTS presented in CCFB3, since without them structural congruence is not included in strong barbed similarity: in the accompanying formalization  we exhibit a pair of structurally congruent processes that are not barbed similar. This conflicts with the intended role of structural congruence as the strongest equivalence between processes, and the proof of the context lemma relies on this specific inclusion. The adoption of the two replication rules for communication is not arbitrary; after all, our LTS follows that in Sangiorgi and Walker’s textbook, modulo late semantics. A popular alternative, found e.g.in [@DBLP:journals/tcs/HonsellMS01; @Bengtson2009], uses a single rule to generate arbitrary copies of the replicated process. We refer to Sangiorgi and Walker for a discussion of the trade-offs between these formulations; the correspondence is understood modulo structural congruence.

None

Following the previous formalizations in [@MillerPI; @DBLP:journals/tcs/HonsellMS01; @DBLP:journals/tocl/TiuM10], in Beluga we separate free steps, where the action does not bind any variable, from bound steps, where the action has a bound variable. Since some rules involve both free and bound actions at the same time, the LF types for free and bound steps are mutually defined. This approach does duplicate some rules, but gets rid of all provisos on free and bound occurrences, which are now taken care of by dependencies (or lack thereof) in second-order process variables. 

2.3 Process Contexts and Structural Congruence↩︎

The notion of (pre)congruence is of paramount importance in the \(\pi\)-calculus: both in the reduction semantics, through structural congruence, and in the study of behavioral equivalence. Informally, a congruence is an equivalence relation that preserves the behavior of the constructors. Often, this is described in textbooks (e.g. [@SWBook]) via the notion of process context: a process where a (non-degenerate) occurrence of 0 is replaced by a hole. Given a context \(C\) and a process \(P\), \(C[P]\) denotes the process obtained by replacing the hole in \(C\) with \(P\). Then, a process precongruence is a binary relation \(\mathcal{R}\) which is a preorder such that if \(P \mathbin{\mathcal{R}} Q\), then, for each context \(C\), \(C[P] \mathbin{\mathcal{R}} C[Q]\).

There is however a peculiarity: since the goal of contexts is to observe how processes behave in every possible environment, they need to be able to capture the free variables in the processes they are filled with. In other words, contexts do not respect \(\alpha\)-equivalence.

This brings in some additional issues with respect to a mechanization, in particular in a HOAS setting, where such entities are a non-starter ¹. A workaround is to close the relation under compatibility ([@Lassen98; @Gay_Vasconcelos_2025]), as described by the rules in our case at the top of Fig. 3. Concretely, when we say that structural congruence is the smallest congruence satisfying the axioms in the bottom of Fig. 3, we are instantiating \(\cal R\) with \(\equiv\).

This is indeed the way structural congruence was formalized as an LF type cong in [@Cecilia24], which we have extended by adding the compatibility and unfolding laws for replication. 

None

There are cases where going the compatibility route is inconvenient, if not plain inadequate, one being the definition of strong barbed (pre)congruence, as we shall see later on, and where contexts must be encoded. In a breakthrough, the authors of [@LancelotAV25] introduced a clever trick to make contexts compatible (no pun intended) with a HOAS encoding, by means of a quaternary relation that implicitly captures the essence of a context:

\[\{(P,P',Q,Q') \mid P'=C[P], \;Q'=C[Q] \;\text{for some context} \;C\}\]

Unlike in the Abella setting where this relation was introduced, a Beluga encoding is rather subtle as the LF contexts must be made explicit. In fact, in general \(\fontfamily{cmss}\selectfont\text{fn}(C[P]) \neq \fontfamily{cmss}\selectfont\text{fn}(P)\), since the binders in \(C\) may capture names that occur free in \(P\), and \(C\) may also introduce names that are fresh for \(P\); while the latter can be avoided by working in an LF context that already contains all free variables of \(P\) and \(C\), the former inevitably leads to a mismatch between the two LF contexts. Therefore, the formalization of this relation cannot be an LF predicate, where all the related terms are defined in an implicit context. Instead, we define the inductive type PCtx in Fig. 4, where the context of the second and fourth processes is a prefix of the context of the first and third processes. 

None

Structural congruence can alternatively be defined as a contextual equivalence via the inductive type Cong in Fig. 5, that uses the type PCtx in the context closure clause. 

None

2.4 Preliminary Lemmas↩︎

We start by establishing some basic properties of the LTS and of process contexts. The former ones can be found in [@SWBook], modulo our choice of late semantics, while the latter ones, adapted from [@LancelotAV25], stem from the implementation of process contexts.

Now for properties of process contexts: some of them would be obvious with the on-paper definition of contexts, but are not trivial in the PCtx formalization. We recall that \(((P,C_P),(Q,C_Q))\) means that there is a context \(C\) such that \(C[P] = C_P\) and \(C[Q] = C_Q\).

As is well known [@Lassen98], a binary relation on processes constitutes a contextual equivalence if and only if it is a compatible equivalence. Because Beluga’s logic lacks support for higher-order predicates, this meta-theorem cannot be generalized; rather, the equivalence must be formalized independently for each specific relation.

The LF definition is more convenient for discussing the properties of the LTS, as in [@Cecilia24], while the inductive one is used later to show the inclusion of structural congruence in another precongruence defined via contexts.

3 Behavioral Equivalences↩︎

Intuitively, two processes can be considered equivalent when they exhibit the same behavior. However, the level of detail at which behaviors can be distinguished depends on the chosen observational granularity; this is where a variety of bisimilarity notions come into play. In CCFB3, the authors focus on strong barbed bisimilarity, which relates processes that can match internal (\(\tau\)) transitions and preserve the same barbs, i.e.the ability to perform input or output on a given channel.

More precisely, the barb, or observability predicate, \(P \downarrow_x\) (resp.\(P \downarrow_{\overline{x}}\)) holds if a process \(P\) can perform an input action with subject \(x\) (resp.an output action with subject \(\overline{x}\)). Following [@SWBook], this notion can be formalized in two equivalent ways, based either on the structure of the process \(P\) or on the (late) LTS:

1. \(P \downarrow_x\) iff \(P \equiv \nu z_1 \dots \nu z_n (x(y).Q \mid R)\) for some \(y,z_1,\dots,z_n,Q,R\), with \(x \notin \{z_1,\dots,z_n\}\). Analogously, \(P \downarrow_{\overline{x}}\) iff \(P \equiv \nu z_1 \dots \nu z_n (\overline{x}y.Q \mid R)\) for some \(y,z_1,\dots,z_n,Q,R\), with \(x \notin \{z_1,\dots,z_n\}\).

   The telescopes, i.e.\(n\)-ary sequences of binders, appearing in this definition of barb are encoded in Beluga by two types barb_in_rew and barb_out_rew, that build the sequence of restrictions incrementally.  Then, the two types encoding barbs identify processes congruent to such telescopes. 

2. \(P \downarrow_x\) iff \(P \xrightarrow{x(z)} P'\) for some \(z,P'\), and similarly \(P \downarrow_{\overline{x}}\) iff \(P \xrightarrow{\overline{x}y} P'\) or \(P \xrightarrow{\overline{x}(z)} P'\) for some \(y,z,P'\).

   We formalize this at the meta level, but it could have been formulated as an LF type as easily. Since the LTS presents one input label and two output labels, Barb_in has one constructor, while Barb_out has two. 

Definitions [def:barb95one] and [def:barb95two] are equivalent, in the sense given by the following lemma. For brevity, we omit some auxiliary technical lemmas and refer to the repository for full details.   

Being invariant w.r.t.the underlying LTS, definition [def:barb95one] can be adopted even in the setting of reduction semantics; however, definition [def:barb95two] has the benefit of being more amenable to mechanized proofs without the need of algebraic rewrites. For this reason, we use the latter in the rest of the development.

A significant property of barbs is that they are preserved by contexts:

We can now give the definition of barbed simulation. A binary relation on processes \(\mathcal{R}\) is a strong barbed simulation if the following conditions hold:

1. \(\mathcal{R}\) is barb preserving: if \(P \mathbin\mathcal{R} Q\) and \(P \downarrow_x\), then \(Q \downarrow_x\); likewise, if \(P \mathbin\mathcal{R} Q\) and \(P \downarrow_{\overline{x}}\), then \(Q \downarrow_{\overline{x}}\).

2. \(\mathcal{R}\) is a reduction simulation: if \(P \mathbin\mathcal{R} Q\) and \(P \xrightarrow{\tau} P'\), then there is \(Q'\) such that \(Q \xrightarrow{\tau} Q'\) and \(P' \mathbin\mathcal{R} Q'\).

The union of all barbed simulations is called strong barbed similarity and will be denoted by \(\mathbin{\overset{\bullet}{\leq}_B}\).

As explained above, barbs are not based on a specific LTS, and, as proven in [@Cecilia24], albeit without the replication operator, early and late semantics provide the same \(\tau\) actions. Thus, our definition of strong barbed similarity turns out to be equivalent to the one based on the early semantics.

(Bi)simulations are perhaps the best known instance of coinductively defined relations. In calculi where the transition relation is well-founded — e.g., those where each transition produces a structurally smaller process, ensuring that every computation trace is finite — (bi)similarity can equivalently be characterized inductively. This is not the case in our fragment of the \(\pi\)-calculus, where infinite behaviors arise due to replication: thus, a genuinely coinductive treatment becomes necessary.

To our rescue, Beluga supports coinductive reasoning in a very flexible way [@ThibodeauCP16]. Coinductive types are defined dually to inductive types: instead of constructors, they are characterized by destructors, or observations. More specifically, while an inductive type is defined by inference rules whose conclusion is an instance of the type, a coinductive type is defined by inference rules where an instance of the type is the premise. Beluga separates this premise from the rest of the rule by using ::.

Reasoning on coinductive objects proceeds via copattern matching. By the Curry-Howard correspondence, proofs by (co)induction are encoded as total (co)recursive functions. In the coinductive case, totality requires coverage of all observations, while productivity ensures that each corecursive call is guarded by an observation; in the (current) absence of a productivity checker in Beluga, this condition must be verified manually. Observations of a coinductive object c are accessed using the syntax c.observation_name, mirroring field access in mainstream programming languages.

As an example of a coinductive definition, we can look at the formalization of strong barbed similarity in Fig. 6, which presents three observations, corresponding to the input barbs, the output barbs and the \(\tau\) transitions. Recall that Beluga does not provide constructs for existential quantification, conjunction, or disjunction, so these must be encoded as inductive types.

None

None

We now recall the notion of strong barbed simulation up to \(\mathbin{\overset{\bullet}{\leq}_B}\), namely a binary relation on processes \(\mathcal{R}\) such that:

1. \(\mathcal{R}\) is barb preserving.

2. if \(P \mathbin\mathcal{R} Q\) and \(P \xrightarrow{\tau} P'\), then there is \(Q'\) such that \(Q \xrightarrow{\tau} Q'\) and \(P' \mathbin{\overset{\bullet}{\leq}_B}\mathbin\mathcal{R} \mathbin{\overset{\bullet}{\leq}_B}Q'\).

As above, strong barbed similarity up to \(\mathbin{\overset{\bullet}{\leq}_B}\) is the union of all strong barbed simulations up to \(\mathbin{\overset{\bullet}{\leq}_B}\).

Again, we cannot develop a general theory of relations up to: we simply encode strong barbed similarity up to \(\mathbin{\overset{\bullet}{\leq}_B}\) as we did for strong barbed similarity — the only difference being in the inductive auxiliary type, which encodes the up to \(\mathbin{\overset{\bullet}{\leq}_B}\). In this setup, strong barbed similarity up to \(\mathbin{\overset{\bullet}{\leq}_B}\) coincides with \(\mathbin{\overset{\bullet}{\leq}_B}\).  The use here of up-to technique is just for convenience: in order to prove that a relation is included in strong barbed similarity, it is sufficient to prove that it is a strong barbed simulation up to \(\mathbin{\overset{\bullet}{\leq}_B}\) and therefore included in barbed similarity up to \(\mathbin{\overset{\bullet}{\leq}_B}\).

3.1 Barbed Precongruence↩︎

One way to distinguish two processes is to observe whether they exhibit the same behavior when placed in the same environment, or context; a desirable property of a (bi)similarity is to be preserved by every possible environment. Unfortunately, strong barbed similarity does not satisfy contextual closure. For instance, the two processes \(\overline{x}y.\overline{a}b.0\) and \(\overline{x}y.0\) are strong barbed similar, since their only barb is \(\downarrow_{\overline{x}}\) and they cannot perform any internal transition. Conversely, plugging them into the context \([\_] \mid x(z).0\) modifies their observable behavior: the former can perform a transition \(\overline{x}y.\overline{a}b.0 \mid x(z).0 \xrightarrow{\tau} \overline{a}b.0 \mid 0\), enabling the observation of a barb \(\downarrow_{\overline{a}}\) that the process \(\overline{x}y.0 \mid x(z).0\), after an internal transition, cannot produce.

Therefore, we aim to identify those pairs of processes whose behavior remains strongly barbed similar under all contexts. The processes \(P\) and \(Q\) are strongly barbed precongruent, denoted by \(P \mathbin{\leq_B}Q\), if, for each context \(C\), \(C[P] \mathbin{\overset{\bullet}{\leq}_B}C[Q]\). 

Among the properties of strong barbed precongruence, the most prominent is its characterization as the largest precongruence included in strong barbed similarity. It turns out that the latter can be formalized as a coinductive definition with only two observations, requiring the inclusion in \(\mathbin{\overset{\bullet}{\leq}_B}\) and the contextual closure. 

The first three proofs immediately follow from the definition of \(\mathbin{\leq_B}\), the fact that \(\mathbin{\overset{\bullet}{\leq}_B}\) is a preorder and context composition; the last two are straightforward coinductive arguments.

4 Context Lemma↩︎

The objective of CCFB3 is to prove that making barbed bisimilarity sensitive to substitutions and parallel composition is sufficient to establish barbed congruence. This result is an instance of a context lemma, namely a characterization of congruence that relaxes the universal quantification on arbitrary contexts, thereby simplifying proofs of congruence.

We recall that substitutions are endofunctions on names with finite support; they can be extended to processes and actions by simultaneously replacing all their free occurrences of names. To encode them, we rely on Beluga’s built-in notion of simultaneous substitutions. In particular, given two Beluga contexts g,h:ctx, a substitution $S:$[h |- g] maps the names in g to names in h; given a process P:[g |- proc] that depends on names in g, the process P[$S]:[h |- proc] is obtained by replacing its names according to $S.

Next, we denote as \(\mathbin{\leq_{\mid s}}\mathrel{\vcenter{:}}= \{ (P,Q) \mid \text{for all} \;R, \sigma, (P \sigma \mid R) \mathbin{\overset{\bullet}{\leq}_B}(Q \sigma \mid R) \}\) the relation obtained by closing barbed similarity under parallel composition and substitutions. Analogously to barbed precongruence, it is formalized by an inductive type BarbPre’. 

The strategy to prove the context lemma consists in showing that \(\mathbin{\leq_{\mid s}}\) is a precongruence included in strong barbed similarity; since, by Lemma [lem:larg95precong], strong barbed precongruence is the largest precongruence included in strong barbed similarity, it follows that \(\mathbin{\leq_{\mid s}}\subseteq \mathbin{\leq_B}\). Below, we detail the results required to complete the proof.

First, an auxiliary lemma describing how transitions of a process \(P\sigma\) arise from transitions of \(P\):

Proving that \(\mathbin{\leq_{\mid s}}\subseteq \mathbin{\overset{\bullet}{\leq}_B}\) is straightforward:

The proof that \(\mathbin{\leq_{\mid s}}\) is a precongruence is trickier and is based on the following result — this is, in fact, the only instance in which coinductive up-to techniques are used.

5 Evaluation↩︎

The entire development comprises approximately 1500 lines of code, organized into nine files. It includes 23 definitions — three of which are coinductive — accounting for roughly \(10\%\) of the total codebase, as well as 53 theorems. Most of these theorems exactly correspond to the relevant results presented in [@SWBook]; however, several of the more intricate ones must be decomposed into multiple statements. This is particularly necessary when they involve combinations of induction and coinduction with differing proof goals. Notably, the only strengthening lemmas required in the Beluga formalization are those already needed at the paper level to satisfy the side conditions of the LTS rules concerning free and bound names. This once again underscores the advantages of using HOAS for handling binders.

A central feature of the \(\pi\)-calculus is its ability to pass names, enabling subprocesses to communicate channel names and subsequently use them. Concretely, input prefixes bind received names, and in all standard semantics there is a transition in which the binder is eliminated and the bound name is replaced by a fresh free name representing the received value. In Beluga, such single substitutions are treated as a special case of simultaneous substitutions, which allows them to be composed seamlessly, as demonstrated in Lemma 10. This is a net gain compared to other approaches (such as [@Bengtson2009]), where the two notions need to be implemented from scratch.

One complication arising from substitutions in Beluga is their interaction with the coverage checker. Verifying coverage often requires solving non-trivial unification problems, which can become more challenging in the presence of substitutions: this is well understood in the theory, but simply not supported yet by the Beluga implementation. Consequently, Lemma 8 is formalized without a totality check. In fairness, we find more urgent the implementation of the productivity checker: for what it is worth, we have manually checked that all coinductive calls comply with productivity, as we understand it, but this falls somewhat short of a complete assurance of the correctness of our mechanization.

In the CCFB paper, the authors stated:

The crux of our challenge is the effective use of coinductive up-to techniques. The intention is that the result should be relatively easy to achieve once the main properties of bisimilarity are established.

However, coinductive up-to techniques, which have a prominent role in the study of other bisimilarities, are only used here once, i.e.to prove the context lemma, and the formalization of strong barbed similarity up to \(\mathbin{\overset{\bullet}{\leq}_B}\) to does not diverge significantly from the formalization of strong barbed similarity. We conclude that the design of the challenge does not exercise significantly the up-to aspect.

6 Related Work↩︎

In this section we mostly concentrate on mechanizations of behavioral equivalence in process calculi.

In [@Bengtson2009; @BengtsonParrow2007Completeness], Bengtson and Parrow provide the largest formalization of the \(\pi\)-calculus in the literature using nominal logic in Isabelle/HOL to represent binders. The encoding of the operational semantics uses commitments [@Milner1993] rather than labelled transitions, i.e. pairs of an action and a derivative process that binds the bound names of the action in the derivative. The treatment of replication follows the single-rule presentation of [@DBLP:journals/tcs/HonsellMS01]. Their results include proving that strong and weak bisimulations, both early and late, are congruences, and that structural congruence is a bisimulation; the authors also provide an axiomatization of strong late bisimulation and prove that it is sound and complete. Coinductive definitions and proofs are encoded by using Isabelle/HOL’s standard coinductive package. Since most of these details are handled by Isabelle, the main focus of Bengtson and Parrow is on the nominal logic aspects of the formalization, which, while elegantly supporting free and bound names, still entails a fair amount of work to establish basic infrastructural properties.

Ambal et al. [@AmbalLS21] provide a Coq formalization of the higher-order \(\pi\)-calculus that systematically studies binder representations for mixed binding (process vs name binders) and establishes strong context bisimilarity as a congruence via Howe’s method. Coinduction is used in the standard way to characterize bisimilarity; coinductive “guarded” proofs only appear in the final step showing that the Howe closure is included in bisimilarity. A direct Coq development in the style of ours would likely require libraries such as PACO [@Hur2013]. Further, the HOAS approach encodes process and name binders in the same way, offering significant simplifications.

In [@TianS20], Tian and Sangiorgi study proof methods for bisimulation in CCS, focusing on contractions rather than equations. They formalize the congruence induced by weak bisimilarity (rooted bisimilarity) in HOL4 using the coinductive package Hol_coreln. Their development does not treat processes up to \(\alpha\)-conversion, and restriction is not a binder; contexts are therefore represented as single-binder \(\lambda\)-expressions applied to processes. As in our work, the coarsest congruence contained in bisimilarity is characterized via closure under composition, although here it is ancillary to the main result on unique solutions of rooted contractions.

Tiu and Miller [@DBLP:journals/tocl/TiuM10] give a proof-search specification of the finite \(\pi\)-calculus in a logic equipped with definitions, fixed points, and the \(\nabla\) quantifier for generic judgments. Their encoding is equivalent to ours w.r.t.syntax and LTS. It does seem more general insofar that the interaction between the \(\forall\), \(\exists\), and \(\nabla\) quantifiers explains the usual distinctions between early, late, and, remarkably, open bisimulation. For the latter the \(\nabla\) quantifier plays a role analogous to Sangiorgi’s distinctions. Veltri and Vezzosi [@VeltriV23] give a much more extensive formalization of process-calculus semantics in Guarded Cubical Agda: they develop fully abstract denotational models for CCS and the early \(\pi\)-calculus, showing that denotational equality coincides with bisimilarity. Their encoding uses well-scoped de Bruijn syntax, in contrast with our HOAS representation in Beluga. Their approach to coinduction is also quite different: guarded recursion, clocks, and cubical path equality provide the semantic infrastructure through which bisimilarity is recovered as equality, whereas we reason directly with coinductive operational relations.

7 Conclusions and Future Work↩︎

What happens if a challenge turns out to be not too challenging? Is it the designers’ fault or the encoders’ merit? In our previous paper we mused on how uneventful the formalization had been. We have to repeat ourselves: the HOAS encoding of the syntax and semantics of the calculus, which we have inherited from a long tradition (dating back to [@MillerPI]), abstracts all the issues related to free and bound names that have preoccupied all first-order encodings. What the present paper brings to the table is a very intensive use of coinductive reasoning: here, Beluga’s copattern approach shines, much more than in a previous coinductive case study (Howe’s method, see [@MomiglianoPT19], which turns out to exercise coinduction only in a limited fashion).

Beluga’s underlying sized types discipline is intrinsically compositional, making nesting coinductive proofs completely unproblematic. This is in sharp contrast with the guarded recursion approach native to Rocq, which would have been simply unfeasible and compelled the user to switch to dedicated libraries such as PACO [@Hur2013]. Again, it is the support for both HOAS and coinduction via observation that makes, in our judgment, the development so smooth — Agda supports a similar approach to coinduction, but not HOAS; Abella offers the converse trade-off.

7.0.0.1 Future Work.

There are several directions in which the present formalization could be extended. A natural first step is to establish the converse direction of the context lemma. The proof presented in [@SWBook] proceeds by constructing a suitable context such that a pair of strongly barbed congruent processes can be composed in parallel under substitution so as to yield strongly barbed bisimilar processes. The argument relies on multi-step internal transitions whose length depends on the size of the support of the substitution. It is not clear to us whether Beluga’s theory of substitution directly captures this style of argument, particularly when it involves a fine-grained analysis of substitutions and their supports. Moreover, the proof makes essential use of the symmetry of strong barbed bisimilarity, so we would have to carry out the symmetric proofs after all.

Open bisimulation is particularly appealing in our setting because Beluga’s contextual objects and simultaneous substitutions seem to provide much of the infrastructure needed to express substitution-closed behavioral relations. The main additional burden would be the treatment of distinctions/freshness constraints and their interaction with the LTS. Since Beluga does not have a \(\nabla\) quantifier, one must prove that the resulting substitution-based relation coincides with the standard distinction-indexed definition, or else identify precisely which variant of open similarity has been mechanized. One possibility to avoid an explicit representation of distinctions could be to look at the theory of quasi-open bisimilarity [@Fu05; @HorneALT18].

Another technically involved extension concerns the coincidence between strong barbed congruence and early congruence. The standard proof requires the introduction of a stratification of strong early bisimilarity, with the key inclusion shown via a contrapositive argument. This reliance on classical reasoning renders a direct mechanization in Beluga particularly challenging.

Finally, Lassen in [@Lassen98] studies contextual closure as the greatest adequate congruence in the context of program equivalence for a functional language. Since adequacy has a barbed “flavor”, the question is whether analogous characterizations can be established for bisimilarity-based congruences in the \(\pi\)-calculus.

Acknowledgments↩︎

This work is partially supported by the National Science Foundation under Grant No. (SHF:Small:Concurrency In Reversible Computations). We thank Brigitte Pientka for several helpful conversations.

AI usage statement. The formalization, definitions, and proofs presented in this paper are entirely the authors’ work. Generative AI tools were used solely for editorial assistance (improving clarity and English wording), and had no role in the technical development or validation of the results.

---

1. HOAS is indeed compatible with weaker notions such as evaluation contexts, i.e., those that do not cross a binder.↩︎