An Open Challenge Problem Repository for Systems Supporting Binders

A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such lib...

Full description

Saved in:
Bibliographic Details
Published in:Electronic proceedings in theoretical computer science 2015-07, Vol.185 (Proc. LFMTP 2015), p.18-32
Main Authors: Felty, Amy, Momigliano, Alberto, Pientka, Brigitte
Format: Article
Language:English
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
cited_by cdi_FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3
cites cdi_FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3
container_end_page 32
container_issue Proc. LFMTP 2015
container_start_page 18
container_title Electronic proceedings in theoretical computer science
container_volume 185
creator Felty, Amy
Momigliano, Alberto
Pientka, Brigitte
description A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.
doi_str_mv 10.4204/EPTCS.185.2
format article
fullrecord <record><control><sourceid>doaj_cross</sourceid><recordid>TN_cdi_doaj_primary_oai_doaj_org_article_d8c7ace32e1f4e2496dc81c64cd08fe0</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><doaj_id>oai_doaj_org_article_d8c7ace32e1f4e2496dc81c64cd08fe0</doaj_id><sourcerecordid>oai_doaj_org_article_d8c7ace32e1f4e2496dc81c64cd08fe0</sourcerecordid><originalsourceid>FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3</originalsourceid><addsrcrecordid>eNpNkEFLwzAUx4MoOOZOfoHcpTNJ0zY5zjJ1MNiw8xzS9KV2dE1J6qHf3m4T8V3e43_48X8_hB4pWXJG-PN6f8iLJRXJkt2gGSNZEjEqyO2_-x4tQjiSaWLJuExnKF91eNdDh_Mv3bbQ1YD33pUtnPAH9C40g_Mjts7jYgwDnAIuvvve-aHpavzSdBX48IDurG4DLH73HH2-rg_5e7TdvW3y1TYynKRDlIERQtvEZoYliUiZtUA5ECF1TEouDdfaSgnSaArcshhkaRm1dKqaUVrGc7S5ciunj6r3zUn7UTndqEvgfK30VMy0oCphMm0gZkAth_OrlRHUpNxURFggE-vpyjLeheDB_vEoUWed6qJTTToVi38AA45oRQ</addsrcrecordid><sourcetype>Open Website</sourcetype><iscdi>true</iscdi><recordtype>article</recordtype></control><display><type>article</type><title>An Open Challenge Problem Repository for Systems Supporting Binders</title><source>ROAD: Directory of Open Access Scholarly Resources</source><creator>Felty, Amy ; Momigliano, Alberto ; Pientka, Brigitte</creator><creatorcontrib>Felty, Amy ; Momigliano, Alberto ; Pientka, Brigitte</creatorcontrib><description>A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.</description><identifier>ISSN: 2075-2180</identifier><identifier>EISSN: 2075-2180</identifier><identifier>DOI: 10.4204/EPTCS.185.2</identifier><language>eng</language><publisher>Open Publishing Association</publisher><ispartof>Electronic proceedings in theoretical computer science, 2015-07, Vol.185 (Proc. LFMTP 2015), p.18-32</ispartof><oa>free_for_read</oa><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3</citedby><cites>FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3</cites></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><link.rule.ids>314,780,784,27924,27925</link.rule.ids></links><search><creatorcontrib>Felty, Amy</creatorcontrib><creatorcontrib>Momigliano, Alberto</creatorcontrib><creatorcontrib>Pientka, Brigitte</creatorcontrib><title>An Open Challenge Problem Repository for Systems Supporting Binders</title><title>Electronic proceedings in theoretical computer science</title><description>A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.</description><issn>2075-2180</issn><issn>2075-2180</issn><fulltext>true</fulltext><rsrctype>article</rsrctype><creationdate>2015</creationdate><recordtype>article</recordtype><sourceid>DOA</sourceid><recordid>eNpNkEFLwzAUx4MoOOZOfoHcpTNJ0zY5zjJ1MNiw8xzS9KV2dE1J6qHf3m4T8V3e43_48X8_hB4pWXJG-PN6f8iLJRXJkt2gGSNZEjEqyO2_-x4tQjiSaWLJuExnKF91eNdDh_Mv3bbQ1YD33pUtnPAH9C40g_Mjts7jYgwDnAIuvvve-aHpavzSdBX48IDurG4DLH73HH2-rg_5e7TdvW3y1TYynKRDlIERQtvEZoYliUiZtUA5ECF1TEouDdfaSgnSaArcshhkaRm1dKqaUVrGc7S5ciunj6r3zUn7UTndqEvgfK30VMy0oCphMm0gZkAth_OrlRHUpNxURFggE-vpyjLeheDB_vEoUWed6qJTTToVi38AA45oRQ</recordid><startdate>20150727</startdate><enddate>20150727</enddate><creator>Felty, Amy</creator><creator>Momigliano, Alberto</creator><creator>Pientka, Brigitte</creator><general>Open Publishing Association</general><scope>AAYXX</scope><scope>CITATION</scope><scope>DOA</scope></search><sort><creationdate>20150727</creationdate><title>An Open Challenge Problem Repository for Systems Supporting Binders</title><author>Felty, Amy ; Momigliano, Alberto ; Pientka, Brigitte</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3</frbrgroupid><rsrctype>articles</rsrctype><prefilter>articles</prefilter><language>eng</language><creationdate>2015</creationdate><toplevel>online_resources</toplevel><creatorcontrib>Felty, Amy</creatorcontrib><creatorcontrib>Momigliano, Alberto</creatorcontrib><creatorcontrib>Pientka, Brigitte</creatorcontrib><collection>CrossRef</collection><collection>DOAJ Directory of Open Access Journals</collection><jtitle>Electronic proceedings in theoretical computer science</jtitle></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext</fulltext></delivery><addata><au>Felty, Amy</au><au>Momigliano, Alberto</au><au>Pientka, Brigitte</au><format>journal</format><genre>article</genre><ristype>JOUR</ristype><atitle>An Open Challenge Problem Repository for Systems Supporting Binders</atitle><jtitle>Electronic proceedings in theoretical computer science</jtitle><date>2015-07-27</date><risdate>2015</risdate><volume>185</volume><issue>Proc. LFMTP 2015</issue><spage>18</spage><epage>32</epage><pages>18-32</pages><issn>2075-2180</issn><eissn>2075-2180</eissn><abstract>A variety of logical frameworks support the use of higher-order abstract syntax in representing formal systems; however, each system has its own set of benchmarks. Even worse, general proof assistants that provide special libraries for dealing with binders offer a very limited evaluation of such libraries, and the examples given often do not exercise and stress-test key aspects that arise in the presence of binders. In this paper we design an open repository ORBI (Open challenge problem Repository for systems supporting reasoning with BInders). We believe the field of reasoning about languages with binders has matured, and a common set of benchmarks provides an important basis for evaluation and qualitative comparison of different systems and libraries that support binders, and it will help to advance the field.</abstract><pub>Open Publishing Association</pub><doi>10.4204/EPTCS.185.2</doi><tpages>15</tpages><oa>free_for_read</oa></addata></record>
fulltext fulltext
identifier ISSN: 2075-2180
ispartof Electronic proceedings in theoretical computer science, 2015-07, Vol.185 (Proc. LFMTP 2015), p.18-32
issn 2075-2180
2075-2180
language eng
recordid cdi_doaj_primary_oai_doaj_org_article_d8c7ace32e1f4e2496dc81c64cd08fe0
source ROAD: Directory of Open Access Scholarly Resources
title An Open Challenge Problem Repository for Systems Supporting Binders
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-28T05%3A05%3A40IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-doaj_cross&rft_val_fmt=info:ofi/fmt:kev:mtx:journal&rft.genre=article&rft.atitle=An%20Open%20Challenge%20Problem%20Repository%20for%20Systems%20Supporting%20Binders&rft.jtitle=Electronic%20proceedings%20in%20theoretical%20computer%20science&rft.au=Felty,%20Amy&rft.date=2015-07-27&rft.volume=185&rft.issue=Proc.%20LFMTP%202015&rft.spage=18&rft.epage=32&rft.pages=18-32&rft.issn=2075-2180&rft.eissn=2075-2180&rft_id=info:doi/10.4204/EPTCS.185.2&rft_dat=%3Cdoaj_cross%3Eoai_doaj_org_article_d8c7ace32e1f4e2496dc81c64cd08fe0%3C/doaj_cross%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c406t-7ec88af5f7c255862ffe14e089a30b49c4aaf99e9ca1e4f23e9bf21f1924711b3%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rfr_iscdi=true