15 citations · 74 across the 20 of their papers we have counts for
3 papers · 1 filter
A Case Study on Logical Relations using Contextual Types
Andrew Cave, Brigitte Pientka
Proofs by logical relations play a key role to establish rich properties such as normalization or contextual equivalence. They are also challenging to mechanize. In this paper, we…
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…