A Beluga Formalization of the Harmony Lemma in the $π$-Calculus
Gabriele Cecilia, Alberto Momigliano
TL;DR
This work formalizes the Harmony Lemma for a π-calculus fragment using Beluga, providing a machine-checked bridge between reduction semantics and labeled transition semantics. By leveraging higher-order abstract syntax, telescope encoding, and lexicographic induction, the authors mechanize both directions of the Harmony equivalence and related equivalences between late and early LTS encodings. The Beluga formalization eliminates boilerplate name-management, showing that much of the intuitive, pen-and-paper reasoning carries over neatly to a machine-checked setting. The results contribute to CC Bench and demonstrate Beluga’s suitability for formalizing concurrent calculi with intricate binding and scope-extrusion features. The work also demonstrates the potential for scalable, mechanized proofs in extensions of the π-calculus and related formal calculi.
Abstract
The "Harmony Lemma", as formulated by Sangiorgi & Walker, establishes the equivalence between the labelled transition semantics and the reduction semantics in the $π$-calculus. Despite being a widely known and accepted result for the standard $π$-calculus, this assertion has never been rigorously proven, formally or informally. Hence, its validity may not be immediately apparent when considering extensions of the $π$-calculus. Contributing to the second challenge of the Concurrent Calculi Formalization Benchmark -- a set of challenges tackling the main issues related to the mechanization of concurrent systems -- we present a formalization of this result for the fragment of the $π$-calculus examined in the Benchmark. Our formalization is implemented in Beluga and draws inspiration from the HOAS formalization of the LTS semantics popularized by Honsell et al. In passing, we introduce a couple of useful encoding techniques for handling telescopes and lexicographic induction.