17 citations · 64 across the 12 of their papers we have counts for
12 papers
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-…
Check: A mechanized metatheory model-checker
James Cheney, Alberto Momigliano
The problem of mechanically formalizing and proving metatheoretic properties of programming language calculi, type systems, operational semantics, and related formal systems has re…
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…