17 citations · 64 across the 12 of their papers we have counts for
11 papers · 1 filter
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…
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…
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…
Towards Substructural Property-Based Testing
Marco Mantovani, Alberto Momigliano
We propose to extend property-based testing to substructural logics to overcome the current lack of reasoning tools in the field. We take the first step by implementing a property-…
An Open Challenge Problem Repository for Systems Supporting Binders
Amy Felty, Alberto Momigliano, Brigitte Pientka
A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, gene…
The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks
Amy P. Felty, Alberto Momigliano, Brigitte Pientka
A variety of logical frameworks support the use of higher-order abstract syntax (HOAS) in representing formal systems. Although these systems seem superficially the same, they diff…
Cut Elimination for a Logic with Induction and Co-induction
Alwen Tiu, Alberto Momigliano
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus…
Induction and Co-induction in Sequent Calculus
Alwen Tiu, Alberto Momigliano
Proof search has been used to specify a wide range of computation systems. In order to build a framework for reasoning about such specifications, we make use of a sequent calculus…
Hybrid: A Definitional Two-Level Approach to Reasoning with Higher-Order Abstract Syntax
Amy Felty, Alberto Momigliano
Combining higher-order abstract syntax and (co)induction in a logical framework is well known to be problematic. Previous work described the implementation of a tool called Hybrid,…
Higher-Order Pattern Complement and the Strict Lambda-Calculus
Alberto Momigliano, Frank Pfenning
We address the problem of complementing higher-order patterns without repetitions of existential variables. Differently from the first-order case, the complement of a pattern canno…