A Beluga Formalization of the Harmony Lemma in the π-Calculus

Gabriele Cecilia
(Università degli Studi di Milano)
Alberto Momigliano
(Università degli Studi di Milano)

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.

In Florian Rabe and Claudio Sacerdoti Coen: Proceedings Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2024), Tallinn, Estonia, 8th July 2024, Electronic Proceedings in Theoretical Computer Science 404, pp. 1–17.
Published: 8th July 2024.

ArXived at: https://dx.doi.org/10.4204/EPTCS.404.1 bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org