English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

A variety of logical frameworks support the use of higher-order abstractsyntax (HOAS) in representing formal systems. Although these systems seemsuperficially the same, they differ in a variety of ways; for example, how theyhandle a context of assumptions and which theorems about a given formal systemcan be concisely expressed and proved. Our contributions in this paper arethree-fold: 1) we develop a common infrastructure for representing benchmarksfor systems supporting reasoning with binders, 2) we present several concretebenchmarks, which highlight a variety of different aspects of reasoning withina context of assumptions, and 3) we design an open repository ORBI, (Openchallenge problem Repository for systems supporting reasoning with BInders).Our work sets the stage for providing a basis for qualitative comparison ofdifferent systems. This allows us to review and survey the state of the art,which we do in great detail for four systems in Part 2 of this paper (Felty etal, 2015). It also allows us to outline future fundamental research questionsregarding the design and implementation of meta-reasoning systems.

The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks