2015/03/20 by Amy Felty, Felty, Amy P., Alberto Momigliano +3 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Natural Language Processing Techniques
paper · pdf · doi:10.48550/arxiv.1503.06095
openalex publication_date 2015/03/20 · openalex created_date 2022/10/01 · openalex updated_date 2026/07/28
A variety of logical frameworks support the use of higher-order abstract\nsyntax (HOAS) in representing formal systems. Although these systems seem\nsuperficially the same, they differ in a variety of ways; for example, how they\nhandle a context of assumptions and which theorems about a given formal system\ncan be concisely expressed and proved. Our contributions in this paper are\nthree-fold: 1) we develop a common infrastructure for representing benchmarks\nfor systems supporting reasoning with binders, 2) we present several concrete\nbenchmarks, which highlight a variety of different aspects of reasoning within\na context of assumptions, and 3) we design an open repository ORBI, (Open\nchallenge problem Repository for systems supporting reasoning with BInders).\nOur work sets the stage for providing a basis for qualitative comparison of\ndifferent systems. This allows us to review and survey the state of the art,\nwhich we do in great detail for four systems in Part 2 of this paper (Felty et\nal, 2015). It also allows us to outline future fundamental research questions\nregarding the design and implementation of meta-reasoning systems.\n