Barbed Similarity for the $\pi$-Calculus in Beluga: A Case Study in Coinductive Reasoning

Lea Trogni, Gabriele Cecilia, Alberto Momigliano

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 ext…