{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:22:22Z","timestamp":1765617742534,"version":"3.48.0"},"publisher-location":"New York, NY, USA","reference-count":19,"publisher":"ACM","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,9,10]]},"DOI":"10.1145\/3756907.3756919","type":"proceedings-article","created":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:11Z","timestamp":1765617551000},"page":"1-13","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Transporting Theorems about Typeability in LF Across Schematically Defined Contexts"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-1275-9721","authenticated-orcid":false,"given":"Chase","family":"Johnson","sequence":"first","affiliation":[{"name":"University of Minnesota, Minneapolis, Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8456-3369","authenticated-orcid":false,"given":"Gopalan","family":"Nadathur","sequence":"additional","affiliation":[{"name":"University of Minnesota, Minneapolis, Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,12,13]]},"reference":[{"key":"e_1_3_3_2_2_2","unstructured":"Michael Ashley-Rollman Karl Crary and Robert Harper. 2005. A solution in Twelf to the PoplMark Challenge problems 1 and 2. Available from the URL https:\/\/www.seas.upenn.edu\/\u00a0plclub\/poplmark\/cmu.html."},{"key":"e_1_3_3_2_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/115418684"},{"key":"e_1_3_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Amy\u00a0P. Felty Alberto Momigliano and Brigitte Pientka. 2015. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations. Journal of Automated Reasoning 55 4 (Dec. 2015) 307\u2013372. 10.1007\/s10817-015-9327-3","DOI":"10.1007\/s10817-015-9327-3"},{"key":"e_1_3_3_2_5_2","unstructured":"Amy\u00a0P. Felty Alberto Momigliano and Brigitte Pientka. 2015. The Next 700 Challenge Problems for Reasoning with Higher-Order Abstract Syntax Representations: Part 1-A Common Infrastructure for Benchmarks. CoRR abs\/1503.06095 (2015) 42\u00a0pages. arXiv:https:\/\/arXiv.org\/abs\/1503.06095http:\/\/arxiv.org\/abs\/1503.06095"},{"key":"e_1_3_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Andrew Gacek Dale Miller and Gopalan Nadathur. 2011. Nominal Abstraction. Information and Computation 209 1 (2011) 48\u201373. 10.1016\/j.ic.2010.09.004","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Robert Harper Furio Honsell and Gordon Plotkin. 1993. A Framework for Defining Logics. J. ACM 40 1 (1993) 143\u2013184. 10.1145\/138027.138060","DOI":"10.1145\/138027.138060"},{"key":"e_1_3_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Robert Harper and Daniel\u00a0R. Licata. 2007. Mechanizing Metatheory in a Logical Framework. Journal of Functional Programming 17 4\u20135 (July 2007) 613\u2013673. 10.1017\/S0956796807006430","DOI":"10.1017\/S0956796807006430"},{"key":"e_1_3_3_2_9_2","unstructured":"Gopalan Nadathur and Mary Southern. 2021. A Logic for Reasoning About LF Specifications. (June 2021). Available from http:\/\/arxiv.org\/abs\/2107.00111.."},{"key":"e_1_3_3_2_10_2","doi-asserted-by":"publisher","DOI":"10.1145\/3551357.3551377"},{"key":"e_1_3_3_2_11_2","doi-asserted-by":"publisher","DOI":"10.1145\/960116.54010"},{"key":"e_1_3_3_2_12_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48660-714"},{"key":"e_1_3_3_2_13_2","volume-title":"Twelf User\u2019s Guide","author":"Pfenning Frank","year":"2002","unstructured":"Frank Pfenning and Carsten Sch\u00fcrmann. 2002. Twelf User\u2019s Guide. Available from http:\/\/www.cs.cmu.edu\/\u00a0twelf\/guide-1-4."},{"key":"e_1_3_3_2_14_2","unstructured":"Frank Pfenning Carsten Sch\u00fcrmann Brigitte Pientka Roberto Virga and Kevin Watkins. [n. d.]. The Twelf Project. http:\/\/twelf.org\/."},{"key":"e_1_3_3_2_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14203-12"},{"key":"e_1_3_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.5555\/932524"},{"key":"e_1_3_3_2_17_2","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.337.8"},{"key":"e_1_3_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2007.01.016"},{"key":"e_1_3_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.5555\/930785"},{"key":"e_1_3_3_2_20_2","doi-asserted-by":"crossref","DOI":"10.21236\/ADA418517","volume-title":"A concurrent logical framework I: Judgments and properties","author":"Watkins Kevin","year":"2003","unstructured":"Kevin Watkins, Iliano Cervesato, Frank Pfenning, and David Walker. 2003. A concurrent logical framework I: Judgments and properties. Technical Report CMU-CS-02-101. Carnegie Mellon University. Revised, May 2003."}],"event":{"name":"PPDP '25: Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming","location":"Rende Italy","acronym":"PPDP '25"},"container-title":["Proceedings of the 27th International Symposium on Principles and Practice of Declarative Programming"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3756907.3756919","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,12,13]],"date-time":"2025-12-13T09:19:54Z","timestamp":1765617594000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3756907.3756919"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,10]]},"references-count":19,"alternative-id":["10.1145\/3756907.3756919","10.1145\/3756907"],"URL":"https:\/\/doi.org\/10.1145\/3756907.3756919","relation":{},"subject":[],"published":{"date-parts":[[2025,9,10]]},"assertion":[{"value":"2025-12-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}