{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T14:40:53Z","timestamp":1758033653111,"version":"3.44.0"},"reference-count":25,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>\n            This article concerns the development of metatheory for extensible languages. It starts with the view that programming languages tailored to specific application domains are to be constructed by composing components from an open library of independently-developed extensions to a host language. In this context, static analyses (such as typing) and dynamic semantics (such as evaluation) are described via relations whose specifications are distributed across the host language and extensions and are given in a rule-based fashion. Metatheoretic properties, which ensure that static analyses accurately gauge runtime behavior, are represented by formulas over such relations. These properties may be fundamental to the language or they may pertain to analyses introduced by individual extensions. We consider the problem of\n            <jats:italic toggle=\"yes\">modular metatheory<\/jats:italic>\n            , by which we mean that proofs of relevant properties should be constructible by reasoning\n            <jats:italic toggle=\"yes\">independently<\/jats:italic>\n            within each component in the library. To solve this problem, we propose the twin ideas of decomposing proofs around language fragments and of reasoning generically about extensions based on broad,\n            <jats:italic toggle=\"yes\">a priori<\/jats:italic>\n            constraints imposed on their behavior. We establish the soundness of these styles of reasoning by showing how complete proofs of the properties can be automatically constructed for any language obtained by composing the independent parts. Precision in these arguments results from framing them within a logic that encodes inductive, rule-based specifications via least fixed-point definitions. We have implemented our ideas in a language specification system called\n            <jats:italic toggle=\"yes\">Sterling<\/jats:italic>\n            \u00a0and a proof assistant called\n            <jats:italic toggle=\"yes\">Extensibella<\/jats:italic>\n            \u00a0and have used them to validate the examples that motivate the theoretical discussions.\n          <\/jats:p>","DOI":"10.1145\/3731555","type":"journal-article","created":{"date-parts":[[2025,5,7]],"date-time":"2025-05-07T12:02:21Z","timestamp":1746619341000},"page":"1-56","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A Modular Approach to Metatheoretic Reasoning for Extensible Languages"],"prefix":"10.1145","volume":"47","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-1924-9466","authenticated-orcid":false,"given":"Dawn","family":"Michaelson","sequence":"first","affiliation":[{"name":"Computer Science and Engineering, University of Minnesota Twin Cities, 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":"Computer Science and Engineering, University of Minnesota Twin Cities, Minneapolis, Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5611-8687","authenticated-orcid":false,"given":"Eric","family":"Van Wyk","sequence":"additional","affiliation":[{"name":"Computer Science and Engineering, University of Minnesota Twin Cities, Minneapolis, Minnesota, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,9,16]]},"reference":[{"key":"e_1_3_3_2_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787\/4650"},{"key":"e_1_3_3_3_1","unstructured":"Benjamin Delaware. 2013. Feature Modularity in Mechanized Reasoning. Ph.\u2009D. thesis. University of Texas Austin Texas. Retrieved from https:\/\/repositories.lib.utexas.edu\/bitstream\/handle\/2152\/22867\/DELAWARE-DISSERTATION-2013.pdf"},{"key":"e_1_3_3_4_1","doi-asserted-by":"crossref","first-page":"595","DOI":"10.1145\/2048066.2048113","volume-title":"Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA)","author":"Delaware Benjamin","year":"2011","unstructured":"Benjamin Delaware, William Cook, and Don Batory. 2011. Product lines of theorems. In Proceedings of the 2011 ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA). ACM, 595\u2013608. DOI: 10.1145\/2048066.2048113"},{"key":"e_1_3_3_5_1","doi-asserted-by":"crossref","first-page":"207","DOI":"10.1145\/2429069.2429094","volume-title":"Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201913)","author":"Delaware Benjamin","year":"2013","unstructured":"Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2013. Meta-Theory \u00e0 La Carte. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL \u201913). ACM, 207\u2013218. DOI: 10.1145\/2429069.2429094"},{"key":"e_1_3_3_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1297027.1297029"},{"key":"e_1_3_3_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048099"},{"key":"e_1_3_3_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.09.004"},{"key":"e_1_3_3_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591286"},{"key":"e_1_3_3_10_1","doi-asserted-by":"publisher","DOI":"10.24926\/2017.188954"},{"key":"e_1_3_3_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3138224"},{"key":"e_1_3_3_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-36089-3_20"},{"key":"e_1_3_3_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136014.3136023"},{"key":"e_1_3_3_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837644"},{"key":"e_1_3_3_15_1","unstructured":"Dawn Michaelson. 2024. Modular Metatheory for Extensible Languages. Ph.\u2009D. thesis. University of Minnesota Minneapolis Minnesota. Retrieved from https:\/\/hdl.handle.net\/11299\/269968"},{"key":"e_1_3_3_16_1","unstructured":"Dawn Michaelson Gopalan Nadathur and Eric Van Wyk. 2023. A modular approach to metatheoretic reasoning for extensible languages. arXiv:2312.14374. Retrieved from https:\/\/arxiv.org\/abs\/2312.14374"},{"key":"e_1_3_3_17_1","unstructured":"Dawn Michaelson Gopalan Nadathur and Eric Van Wyk. 2024. Modular Metatheory for Extensible Languages Webpage. Retrieved from http:\/\/mmel.cs.umn.edu"},{"key":"e_1_3_3_18_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2002.3103"},{"key":"e_1_3_3_19_1","volume-title":"Proceedings of the 1st Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, the 11th ACM SIGPLAN International Conference on Functional Programming","author":"Mulhern Anne","year":"2006","unstructured":"Anne Mulhern. 2006. Proof weaving. In Proceedings of the 1st Informal ACM SIGPLAN Workshop on Mechanizing Metatheory, the 11th ACM SIGPLAN International Conference on Functional Programming."},{"key":"e_1_3_3_20_1","volume-title":"Types and Programming Languages","author":"Benjamin C.","year":"2002","unstructured":"Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press."},{"key":"e_1_3_3_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_3_3_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2428116.2428120"},{"key":"e_1_3_3_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542476.1542499"},{"key":"e_1_3_3_24_1","unstructured":"Alwen Tiu. 2004. A Logical Framework for Reasoning about Logical Specifications. Ph.\u2009D. thesis. Pennsylvania State University. Retrieved from http:\/\/etda.libraries.psu.edu\/theses\/approved\/WorldWideIndex\/ETD-479\/"},{"key":"e_1_3_3_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45937-5_11"},{"key":"e_1_3_3_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2009.07.004"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3731555","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,9,16]],"date-time":"2025-09-16T14:02:56Z","timestamp":1758031376000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3731555"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,16]]},"references-count":25,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3731555"],"URL":"https:\/\/doi.org\/10.1145\/3731555","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2025,9,16]]},"assertion":[{"value":"2024-04-09","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-20","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-09-16","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}