{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T18:11:32Z","timestamp":1760033492306,"version":"build-2065373602"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T00:00:00Z","timestamp":1759968000000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100023581","name":"National Science Foundation Graduate Research Fellowship Program","doi-asserted-by":"crossref","award":["2141064"],"award-info":[{"award-number":["2141064"]}],"id":[{"id":"10.13039\/100023581","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the languages and compilers that they support. Contextual equivalence is difficult to work with directly, and both logical relations and transition system-based approaches typically fix a specific notion of effect globally. While modular transition systems have been effective in imperative settings, they are suboptimal for functional code. These limitations restrict the extension and composition of semantics in these systems. In Pyrosome, verified compilers are fully extensible, meaning that to extend a language simply requires defining and verifying the compilation of the new feature, reusing the old correctness theorem for all other cases. The novel enabling idea is an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler.<\/jats:p>\n          <jats:p>Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by dependently sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. We support vertical composition of any compilers expressed in our framework in addition to feature extension. Since our design requires compilers to support open programs, our correctness guarantees support linking with any target code of the appropriate type. As a case study, we present a multipass compiler from System F with simple references, through CPS translation and closure conversion. Specifically, we demonstrate how we can build such a compiler incrementally by starting with a compiler for simply typed lambda-calculus and adding natural numbers, the unit type, recursive functions, and a global heap, then extending judgments with a type environment and adding type abstraction, all while reusing the original theorems. We also present a linear version of the simply typed CPS pass and compile a small imperative language to the simply typed target to show how Pyrosome handles substructural typing and imperative features.<\/jats:p>","DOI":"10.1145\/3763052","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"58-85","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Pyrosome: Verified Compilation for Modular Metatheory"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0700-3514","authenticated-orcid":false,"given":"Dustin","family":"Jamner","sequence":"first","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0005-6415-7423","authenticated-orcid":false,"given":"Gabriel","family":"Kammer","sequence":"additional","affiliation":[{"name":"Intel, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9874-0159","authenticated-orcid":false,"given":"Ritam","family":"Nag","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7085-9417","authenticated-orcid":false,"given":"Adam","family":"Chlipala","sequence":"additional","affiliation":[{"name":"Massachusetts Institute of Technology, Cambridge, USA"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96712"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.SNAPL.2015.15"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034773.2034830"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236785"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674652"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/982962.964003"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290335"},{"key":"e_1_2_1_8_1","volume-title":"Workshop on Principles of Secure Compilation. ACM","author":"Bowman William J","year":"2021","unstructured":"William J Bowman. 2021. Compilation as Multi-Language Semantics. In Workshop on Principles of Secure Compilation. ACM, New York, NY, USA."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(86)90053-9"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_23"},{"volume-title":"A General Approach to Define Binders Using Matching Logic","author":"Chen Xiaohong","key":"e_1_2_1_11_1","unstructured":"Xiaohong Chen and Grigore Ro\u015fu. 2020. A General Approach to Define Binders Using Matching Logic. University of Illinois at Urbana-Champaign."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706312"},{"key":"e_1_2_1_13_1","volume-title":"d. S. Oliveira, and Tom Schrijvers","author":"Delaware Benjamin","year":"2013","unstructured":"Benjamin Delaware, Bruno C. d. S. Oliveira, and Tom Schrijvers. 2013. Meta-theory \u00e0 La Carte. In POPL (2013). ACM, 207\u2013218. isbn:978-1-4503-1832-7"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837618"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60579-7"},{"key":"e_1_2_1_17_1","first-page":"2021","article-title":"Integration Verification Across Software and Hardware for a Simple Embedded System","volume":"21","author":"Erbsen Andres","year":"2021","unstructured":"Andres Erbsen, Samuel Gruetter, Joonwon Choi, Clark Wood, and Adam Chlipala. 2021. Integration Verification Across Software and Hardware for a Simple Embedded System. In PLDI. 21, 2021.","journal-title":"PLDI."},{"key":"e_1_2_1_18_1","volume-title":"On the expressive power of programming languages. Science of computer programming, 17, 1-3","author":"Felleisen Matthias","year":"1991","unstructured":"Matthias Felleisen. 1991. On the expressive power of programming languages. Science of computer programming, 17, 1-3 (1991), 35\u201375."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498715"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/138027.138060"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","unstructured":"Dustin Jamner Gabriel Kammer and Ritam Nag. 2025. Pyrosome. https:\/\/doi.org\/10.5281\/zenodo.15762503 10.5281\/zenodo.15762503","DOI":"10.5281\/zenodo.15762503"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837642"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290315"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454097"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_26_1","volume-title":"ERTS","author":"Leroy Xavier","year":"2016","unstructured":"Xavier Leroy, Sandrine Blazy, Daniel K\u00e4stner, Bernhard Schommer, Markus Pister, and Christian Ferdinand. 2016. CompCert \u2013 A Formally Verified Optimizing Compiler. In ERTS 2016. SEE."},{"key":"e_1_2_1_27_1","volume-title":"John Power, and Hayo Thielecke","author":"Levy PaulBlain","year":"2003","unstructured":"PaulBlain Levy, John Power, and Hayo Thielecke. 2003. Modelling environments in call-by-value programming languages. Information and computation, 185, 2 (2003), 182\u2013210."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473579"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.46298\/entics.14666"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3354166.3354181"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1498926.1498930"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/237721.237791"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951941"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341689"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3519939.3523703"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_8"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45931-6_24"},{"key":"e_1_2_1_39_1","volume-title":"LCF considered as a programming language. Theoretical computer science, 5, 3","author":"Plotkin Gordon D.","year":"1977","unstructured":"Gordon D. Plotkin. 1977. LCF considered as a programming language. Theoretical computer science, 5, 3 (1977), 223\u2013255."},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2010.03.012"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3571220"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-22102-1_24"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294101"},{"key":"e_1_2_1_44_1","unstructured":"Jonathan Sterling. 2019. Algebraic Type Theory and Universe Hierarchies. https:\/\/arxiv.org\/pdf\/1902.08848"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/2660193.2660201"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434304"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3054.001.0001"},{"key":"e_1_2_1_49_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Zakowski Yannick","year":"2019","unstructured":"Li-yao Xia, Yannick Zakowski, Paul He, Chung-Kil Hur, Gregory Malecha, Benjamin C Pierce, and Steve Zdancewic. 2019. Interaction trees: representing recursive and impure programs in Coq. Proceedings of the ACM on Programming Languages, 4, POPL (2019), 1\u201332."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/3632914"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591239"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763052","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763052","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T17:41:19Z","timestamp":1760031679000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763052"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":52,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763052"],"URL":"https:\/\/doi.org\/10.1145\/3763052","relation":{},"ISSN":["2475-1421"],"issn-type":[{"type":"electronic","value":"2475-1421"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2024-10-16","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}