Benchmarks
We present several benchmark problems. All these examples are purposefully simple, so they can be easily understood and one can quickly appreciate the capabilities and trade-offs different systems offer. Yet we believe they are representative for issues and problems arising when formalizing formal systems and proofs about them. All of them revolve around the lambda-calculus.
A longer discussion on this can be found in Reasoning with Higher-Order Abstract Syntax and Contexts: A Comparison by Amy Felty and Brigitte Pientka, to appear at ITP-10. We also provide an electronic appendix with all the definitions and theorems (appendix).
Solutions implemented in the Twelf system
- Reasoning about declarative and algorithmic equality (config file, elf file)
- Subject reduction for simply typed lambda-calculus (config file, elf file)
- Type unicity (config file, elf file)
- Reasoning about shapes of lambda-terms (config file, elf file)
Solutions implemented in Beluga
Most of the challenge problems are discussed in the tutorial for Beluga. We list them individually below.
- Reasoning about declarative and algorithmic equality
(beluga file)
see also Tutorial 4. Equality reasoning - Subject reduction for simply typed lambda-calculus
(beluga file)
see also Tutorial 3. Subject reduction - Type unicity (beluga file)
see also Tutorial 1. Type uniqueness - Reasoning about shapes of lambda-terms (beluga file)
- Path example (beluga file)
see also Tutorial 2. Reasoning about paths in lambda-terms - Reasoning about "smaller" relation on lambda-terms (beluga file)
see also Tutorial 5. Reasoning about "smaller" relation on lambda-terms
Solutions in two-level Hybrid
Please see Two-level Hybrid: Case studies.