2 citations · 3 across the 3 of their papers we have counts for
3 papers
cs.LO2026
Barbed Similarity for the -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…
cs.LO2025★ 1 cited
A Formalization of the Reversible Concurrent Calculus CCSKP in Beluga
Gabriele Cecilia
Reversible concurrent calculi are abstract models for concurrent systems in which any action can potentially be undone. Over the last few decades, different formalisms have been de…
cs.LO2024★ 2 cited
A Beluga Formalization of the Harmony Lemma in the -Calculus
Gabriele Cecilia, Alberto Momigliano
The "Harmony Lemma", as formulated by Sangiorgi & Walker, establishes the equivalence between the labelled transition semantics and the reduction semantics in the -calculus. Des…