17 citations · 64 across the 12 of their papers we have counts for
Showing 2024Show all
3 papers · 1 filter
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…
cs.LO2024★ 1 cited
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…
cs.LO2024
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…