{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,15]],"date-time":"2026-07-15T21:23:21Z","timestamp":1784150601394,"version":"3.55.0"},"reference-count":38,"publisher":"Cambridge University Press (CUP)","issue":"9","license":[{"start":{"date-parts":[[2017,5,5]],"date-time":"2017-05-05T00:00:00Z","timestamp":1493942400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2018,10]]},"abstract":"<jats:p>A variety of logical frameworks supports the use of higher order abstract syntax in representing formal systems. Although these systems seem superficially the same, they differ in a variety of ways, for example, how they handle a<jats:italic>context<\/jats:italic>of assumptions and which theorems about a given formal system can be concisely expressed and proved. Our contributions in this paper are two-fold: (1) We develop a common infrastructure and language for describing benchmarks for systems supporting reasoning with binders, and (2) we present several concrete benchmarks, which highlight a variety of different aspects of reasoning within a context of assumptions. Our work provides the background for the qualitative comparison of different systems that we have completed in a separate paper. It also allows us to outline future fundamental research questions regarding the design and implementation of meta-reasoning systems.<\/jats:p>","DOI":"10.1017\/s0960129517000093","type":"journal-article","created":{"date-parts":[[2017,5,5]],"date-time":"2017-05-05T04:43:51Z","timestamp":1493959431000},"page":"1507-1540","source":"Crossref","is-referenced-by-count":14,"title":["Benchmarks for reasoning with syntax trees containing binders and contexts of assumptions"],"prefix":"10.1017","volume":"28","author":[{"given":"AMY","family":"FELTY","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0942-4777","authenticated-orcid":false,"given":"ALBERTO","family":"MOMIGLIANO","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"BRIGITTE","family":"PIENTKA","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2017,5,5]]},"reference":[{"key":"S0960129517000093_ref36","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9143-8"},{"key":"S0960129517000093_ref37","doi-asserted-by":"crossref","unstructured":"Wang Y. , Chaudhuri K. , Gacek A. and Nadathur G. (2013). Reasoning about higher-order relational specifications. In: Proceedings of the 15th International ACM SIGPLAN Symposium on Principles and Practice of Declarative Programming, ACM Press, 157\u2013168.","DOI":"10.1145\/2505879.2505889"},{"key":"S0960129517000093_ref35","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann C. and Sarnat J. (2008). Structural logical relations. In: Proceedings of the 23rd Annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society, 69\u201380.","DOI":"10.1109\/LICS.2008.44"},{"key":"S0960129517000093_ref2","doi-asserted-by":"crossref","unstructured":"Cave A. and Pientka B. (2012). Programming with binders and indexed data-types. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, ACM Press, 413\u2013424.","DOI":"10.1145\/2103656.2103705"},{"key":"S0960129517000093_ref8","doi-asserted-by":"crossref","unstructured":"Felty A.P. , Momigliano A. and Pientka B. (2015b). An open challenge problem repository for systems supporting binders. In: Proceedings of the 10th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Electronic Proceedings in Theoretical Computer Science, vol. 185, pages 18\u201332.","DOI":"10.4204\/EPTCS.185.2"},{"key":"S0960129517000093_ref20","doi-asserted-by":"crossref","unstructured":"Momigliano A. (2012). A supposedly fun thing I may have to do again: A HOAS encoding of Howe's method. In: Proceedings of the 7th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-Languages, Theory and Practice, ACM Press, 33\u201342.","DOI":"10.1145\/2364406.2364411"},{"key":"S0960129517000093_ref11","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9218-1"},{"key":"S0960129517000093_ref22","doi-asserted-by":"crossref","unstructured":"Momigliano A. , Martin A.J. and Felty A.P. (2008). Two-level Hybrid: A system for reasoning using higher-order abstract syntax. In: Proceedings of the 2nd International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2008, Electronic Notes in Theoretical Computer Science, vol. 196, Elsevier, 85\u201393.","DOI":"10.1016\/j.entcs.2007.09.019"},{"key":"S0960129517000093_ref25","doi-asserted-by":"crossref","unstructured":"Pientka B. (2008). A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions. In: Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, ACM Press, 371\u2013382.","DOI":"10.1145\/1328438.1328483"},{"key":"S0960129517000093_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-010-9194-x"},{"key":"S0960129517000093_ref31","doi-asserted-by":"crossref","unstructured":"Poswolsky A. B. and Sch\u00fcrmann C. (2008). Practical programming with higher-order encodings and dependent types. In: Proceedings of the 17th European Symposium on Programming, Lecture Notes in Computer Science, vol. 4960, Springer, 93\u2013107.","DOI":"10.1007\/978-3-540-78739-6_7"},{"key":"S0960129517000093_ref24","doi-asserted-by":"crossref","unstructured":"Pientka B. (2007). Proof pearl: The power of higher-order encodings in the logical framework LF. In: Proceedings of the 20th International Conference on Theorem Proving in Higher-Order Logics, Lecture Notes in Computer Science, Springer, 246\u2013261.","DOI":"10.1007\/978-3-540-74591-4_19"},{"key":"S0960129517000093_ref10","doi-asserted-by":"crossref","unstructured":"Gacek A. (2008). The Abella interactive theorem prover (system description). In: Proceedings of the 4th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, vol. 5195, 154\u2013161.","DOI":"10.1007\/978-3-540-71070-7_13"},{"key":"S0960129517000093_ref28","doi-asserted-by":"crossref","unstructured":"Pientka B. and Dunfield J. (2010). Beluga: A framework for programming and reasoning with deductive systems (system description). In: Proceedings of the 5th International Joint Conference on Automated Reasoning, Lecture Notes in Computer Science, vol. 6173, Springer, 15\u201321.","DOI":"10.1007\/978-3-642-14203-1_2"},{"key":"S0960129517000093_ref6","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9327-3"},{"key":"S0960129517000093_ref13","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"S0960129517000093_ref21","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80506-1"},{"key":"S0960129517000093_ref14","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006430"},{"key":"S0960129517000093_ref16","first-page":"11","article-title":"On the meanings of the logical constants and the justifications of the logical laws","volume":"1","author":"Martin-L\u00f6f","year":"1996","journal-title":"Nordic Journal of Philosophical Logic"},{"key":"S0960129517000093_ref3","doi-asserted-by":"crossref","unstructured":"Cave A. and Pientka B. (2015). A case study on logical relations using contextual types. In: Proceedings of the 10th International Workshop on Logical Frameworks and Meta Languages: Theory and Practice, LFMTP 2015, Electronic Proceedings in Theoretical Computer Science, vol. 185, 33\u201345.","DOI":"10.4204\/EPTCS.185.3"},{"key":"S0960129517000093_ref12","volume-title":"Proofs and Types","author":"Girard","year":"1990"},{"key":"S0960129517000093_ref38","doi-asserted-by":"crossref","unstructured":"Wang Y. and Nadathur G. (2013). Towards extracting explicit proofs from totality checking in Twelf. In: Proceedings of the 8th ACM SIGPLAN International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, ACM Press, 55\u201366.","DOI":"10.1145\/2503887.2503893"},{"key":"S0960129517000093_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-011-9217-2"},{"key":"S0960129517000093_ref4","doi-asserted-by":"crossref","unstructured":"Claessen K. , Johansson M. , Ros\u00e9n D. and Smallbone N. (2015). TIP: Tons of inductive problems. In: Kerber M. , Carette J. , Kaliszyk C. , Rabe F. and Sorge V. (eds.) Proceedings of the Intelligent Computer Mathematics - International Conference, CICM 2015, Washington, DC, USA, July 13\u201317, 2015, Lecture Notes in Computer Science, vol. 9150, Springer, 333\u2013337.","DOI":"10.1007\/978-3-319-20615-8_23"},{"key":"S0960129517000093_ref32","unstructured":"Sch\u00fcrmann C. (2000). Automating the Meta Theory of Deductive Systems. PhD thesis, Department of Computer Science, Carnegie Mellon University. Available as Technical Report CMU-CS-00-146."},{"key":"S0960129517000093_ref19","doi-asserted-by":"crossref","first-page":"411","DOI":"10.1007\/3-540-44622-2_28","volume-title":"Computer Sceince Logic","author":"Momigliano","year":"2000"},{"key":"S0960129517000093_ref29","volume-title":"Types and Programming Languages","author":"Pierce","year":"2002"},{"key":"S0960129517000093_ref34","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann C. and Pfenning F. (2003). A coverage checking algorithm for LF. In: Prceedings 16th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 2758, Springer, 120\u2013135.","DOI":"10.1007\/10930755_8"},{"key":"S0960129517000093_ref23","unstructured":"Pfenning F. (2001). Computation and deduction. http:\/\/www.cs.cmu.edu\/~fp\/courses\/compded\/handouts\/cd.pdf, Accessed 26 October 2016."},{"key":"S0960129517000093_ref33","doi-asserted-by":"crossref","unstructured":"Sch\u00fcrmann C. (2009). The Twelf proof assistant. In: Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 5674, Springer, 79\u201383.","DOI":"10.1007\/978-3-642-03359-9_7"},{"key":"S0960129517000093_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9254-5"},{"key":"S0960129517000093_ref18","doi-asserted-by":"publisher","DOI":"10.1145\/333580.333590"},{"key":"S0960129517000093_ref1","doi-asserted-by":"crossref","unstructured":"Aydemir B.E. , Bohannon A. , Fairbairn M. , Foster J.N. , Pierce B.C. , Sewell P. , Vytiniotis D. , Washburn G. , Weirich S. and Zdancewic S. (2005). Mechanized metatheory for the masses: The poplmark challenge. In: Proceedings of the 18th International Conference on Theorem Proving in Higher Order Logics, Lecture Notes in Computer Science, vol. 3603, Springer, 50\u201365.","DOI":"10.1007\/11541868_4"},{"key":"S0960129517000093_ref26","unstructured":"Pientka B. and Cave A. (2015). Inductive Beluga: Programming proofs (system description). In: Felty A.P . and Middeldorp A. (eds.) Proceedings of the 25th International Conference on Automated Deduction (CADE-25), Lecture Notes in Computer Science, vol. 9195, Springer, 272\u2013281."},{"key":"S0960129517000093_ref5","doi-asserted-by":"crossref","unstructured":"Crary K. (2009). Explicit contexts in LF (extended abstract). In: Proceedings of the 3rd International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, LFMTP 2008, Electronic Proceedings in Theoretical Computer Science, vol. 228, Elsevier, 53\u201368.","DOI":"10.1016\/j.entcs.2008.12.116"},{"key":"S0960129517000093_ref27","doi-asserted-by":"crossref","unstructured":"Pientka B. and Dunfield J. (2008). Programming with proofs and explicit contexts. In: Proceedings of the 10th ACM SIGPLAN International Conference on Principles and Practice of Declarative Programming, ACM Press, 163\u2013173.","DOI":"10.1145\/1389449.1389469"},{"key":"S0960129517000093_ref15","first-page":"283","volume-title":"SAT 2000: Highlights of Satisfiability Research in the Year 2000","author":"Hoos","year":"2000"},{"key":"S0960129517000093_ref17","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/1.4.497"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129517000093","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,23]],"date-time":"2019-09-23T07:19:43Z","timestamp":1569223183000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129517000093\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,5,5]]},"references-count":38,"journal-issue":{"issue":"9","published-print":{"date-parts":[[2018,10]]}},"alternative-id":["S0960129517000093"],"URL":"https:\/\/doi.org\/10.1017\/s0960129517000093","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,5,5]]}}}