Barbed Similarity for the π-Calculus in Beluga: A Case Study in Coinductive Reasoning

We formalize strong barbed similarity for the π-calculus in the Beluga proof assistant, completing a line of work addressing the Concurrent Calculi Formalization Benchmark.By extending previous developments to include replication, we give a coinductive encoding of behavioral equivalence based on barbs and internal actions.Using Beluga's copattern-based coinduction, we obtain concise and compositional proofs, including compatibility properties and a context lemma characterizing barbed precongruence.The case study demonstrates the effectiveness of combining HOAS and coinductive reasoning for mechanizing concurrent calculi. SyntaxWe 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, QRecall that the input prefix x(y).P and the restriction (ν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 LF names: type =;