Barbed Similarity for the -Calculus in Beluga: A Case Study in Coinductive Reasoning
arXiv:2607.12652 · doi:10.4204/EPTCS.448.1
Abstract
We formalize strong barbed similarity for the pi-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.
In Proceedings LFMTP 2026, arXiv:2607.10318