From the 1 of 4 linked papers with an AI index.
4 papers
Barbed Similarity for the -Calculus in Beluga: A Case Study in Coinductive Reasoning
Lea Trogni, Gabriele Cecilia, Alberto Momigliano
The paper formalizes strong barbed similarity for the pi‑calculus in the Beluga proof assistant, using coinductive and copattern‑based techniques to obtain concise proofs of behavi…
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. De…
Property-Based Testing by Elaborating Proof Outlines
Dale Miller, Alberto Momigliano
Property-based testing (PBT) is a technique for validating code against an executable specification by automatically generating test-data. We present a proof-theoretical reconstruc…
More Church-Rosser Proofs in BELUGA
Alberto Momigliano, Martina Sassella
We report on yet another formalization of the Church-Rosser property in lambda-calculi, carried out with the proof environment Beluga. After the well-known proofs of confluence for…