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

Solutions implemented in Beluga

Most of the challenge problems are discussed in the tutorial for Beluga. We list them individually below.

Solutions in two-level Hybrid

Please see Two-level Hybrid: Case studies.