Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions

摘要

A variety of logical frameworks supports the use of higher order abstract syntax inrnrepresenting formal systems. Although these systems seem superficially the same, they differrnin a variety of ways, for example, how they handle a context of assumptions and whichrntheorems about a given formal system can be concisely expressed and proved. Ourrncontributions in this paper are two-fold: (1) We develop a common infrastructure andrnlanguage for describing benchmarks for systems supporting reasoning with binders, and (2)rnwe present several concrete benchmarks, which highlight a variety of different aspects ofrnreasoning within a context of assumptions. Our work provides the background for thernqualitative comparison of different systems that we have completed in a separate paper. Itrnalso allows us to outline future fundamental research questions regarding the design andrnimplementation of meta-reasoning systems.