{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:10:05Z","timestamp":1784196605497,"version":"3.55.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>Certified compilers are complex software systems. Like other large systems, they demand modular, extensible designs. While there has been progress in extensible metatheory mechanization, scaling extensibility and reuse to meet the demands of full compiler verification remains a major challenge.<\/jats:p>\n                  <jats:p>\n                    We respond to this challenge by introducing novel expressive power to a proof language. Our language design equips the Rocq prover with an extensibility mechanism inspired by the object-oriented ideas of late binding, mixin composition, and family polymorphism. We implement our design as a plugin for Rocq, called Rocqet. We identify strategies for using Rocqet\u2019s new expressive power to modularize the monolithic design of large certified developments as complex as the CompCert compiler. The payoff is a high degree of modularity and reuse in the formalization of intermediate languages, ISAs, compiler transformations, and compiler extensions, with the ability to compose these reusable components\u2014certified compilers\n                    <jats:italic toggle=\"yes\">\u00e0 la carte.<\/jats:italic>\n                    We report significantly improved proof-compilation performance compared to earlier work on extensible metatheory mechanization. We also report good performance of the extracted compiler.\n                  <\/jats:p>","DOI":"10.1145\/3729261","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"372-395","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Certified Compilers \u00e0 la Carte"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0002-1951-7424","authenticated-orcid":false,"given":"Oghenevwogaga","family":"Ebresafe","sequence":"first","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0007-3786-2711","authenticated-orcid":false,"given":"Ian","family":"Zhao","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7389-8921","authenticated-orcid":false,"given":"Ende","family":"Jin","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-9041-4698","authenticated-orcid":false,"given":"Arthur","family":"Bright","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-8076-3610","authenticated-orcid":false,"given":"Charles","family":"Jian","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8206-4694","authenticated-orcid":false,"given":"Yizhou","family":"Zhang","sequence":"additional","affiliation":[{"name":"University of Waterloo, Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796801004257"},{"key":"e_1_3_2_3_2","doi-asserted-by":"publisher","unstructured":"Don Batory Peter H\u00f6fner and Jongwook Kim. 2011. Feature interactions products and composition. In ACM Int\u2019l Conf. on Generative Programming and Component Engineering (GPCE). https:\/\/doi.org\/10.1145\/2047862.2047867 doi:10.1145\/2047862.2047867","DOI":"10.1145\/2047862.2047867"},{"key":"e_1_3_2_4_2","doi-asserted-by":"publisher","unstructured":"Gilad Bracha and William Cook. 1990. Mixin-based inheritance. In ACM SIGPLAN Conf. on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/97945.97982 doi:10.1145\/97945.97982","DOI":"10.1145\/97945.97982"},{"key":"e_1_3_2_5_2","doi-asserted-by":"publisher","unstructured":"William R. Cook Walter L. Hill and Peter S. Canning. 1990. Inheritance is not subtyping. In ACM SIGPLAN Symp. on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/96709.96721 doi:10.1145\/96709.96721","DOI":"10.1145\/96709.96721"},{"key":"e_1_3_2_6_2","doi-asserted-by":"publisher","unstructured":"Laurence E. Day and Graham Hutton. 2013. Compilation \u00e0 la carte. In Symp. on Implementation and Application of Functional Languages (IFL). https:\/\/doi.org\/10.1145\/2620678.2620680 doi:10.1145\/2620678.2620680","DOI":"10.1145\/2620678.2620680"},{"key":"e_1_3_2_7_2","doi-asserted-by":"publisher","unstructured":"Benjamin Delaware William Cook and Don Batory. 2011. Product lines of theorems. In ACM SIGPLAN Conf. on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/2076021.2048113 doi:10.1145\/2076021.2048113","DOI":"10.1145\/2076021.2048113"},{"key":"e_1_3_2_8_2","doi-asserted-by":"publisher","unstructured":"Benjamin Delaware Bruno C. d. S. Oliveira and Tom Schrijvers. 2013. Meta-theory \u00e0 la carte. In ACM SIGPLAN Symp. on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2429069.2429094 doi:10.1145\/2429069.2429094","DOI":"10.1145\/2429069.2429094"},{"key":"e_1_3_2_9_2","doi-asserted-by":"publisher","unstructured":"Benjamin Delaware Steven Keuchel Tom Schrijvers and Bruno C.d.S. Oliveira. 2013. Modular monadic meta-theory. In ACM SIGPLAN Conf. on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/2500365.2500587 doi:10.1145\/2500365.2500587","DOI":"10.1145\/2500365.2500587"},{"key":"e_1_3_2_10_2","doi-asserted-by":"publisher","unstructured":"Dominic Duggan and Constantinos Sourelis. 1996. Mixin modules. In ACM SIGPLAN Conf. on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/232627.232654 doi:10.1145\/232627.232654","DOI":"10.1145\/232627.232654"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"Oghenevwogaga Ebresafe Ian Zhao Ende Jin Arthur Bright Charles Jian and Yizhou Zhang. 2025. Certified Compilers \u00e0 la Carte (Artifact). https:\/\/doi.org\/10.5281\/zenodo.15052648. https:\/\/doi.org\/10.5281\/zenodo.15052648 doi:10.5281\/zenodo.15052648","DOI":"10.5281\/zenodo.15052648"},{"key":"e_1_3_2_12_2","volume-title":"Technical Report CS-2025-02","author":"Ebresafe Oghenevwogaga","year":"2025","unstructured":"Oghenevwogaga Ebresafe, Ian Zhao, Ende Jin, Arthur Bright, Charles Jian, and Yizhou Zhang. 2025. Certified Compilers \u00e0 la Carte (Extended Version). Technical Report CS-2025-02. School of Computer Science, University of Waterloo."},{"key":"e_1_3_2_13_2","doi-asserted-by":"publisher","unstructured":"Erik Ernst. 2001. Family polymorphism. In European Conf. on Object-Oriented Programming (ECOOP). https:\/\/doi.org\/10.1007\/3-540-45337-7_17 doi:10.1007\/3-540-45337-7_17","DOI":"10.1007\/3-540-45337-7_17"},{"key":"e_1_3_2_14_2","doi-asserted-by":"publisher","unstructured":"Matthew Flatt Shriram Krishnamurthi and Matthias Felleisen. 1998. Classes and mixins. In ACM SIGPLAN Symp. on Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/268946.268961 doi:10.1145\/268946.268961","DOI":"10.1145\/268946.268961"},{"key":"e_1_3_2_15_2","doi-asserted-by":"publisher","unstructured":"Yannick Forster and Kathrin Stark. 2020. Coq \u00e0 la carte: A practical approach to modular syntax with binders. In ACM SIGPLAN Conf. on Certified Programs and Proofs (CPP). https:\/\/doi.org\/10.1145\/3372885.3373817 doi:10.1145\/3372885.3373817","DOI":"10.1145\/3372885.3373817"},{"key":"e_1_3_2_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-024-09705-6"},{"key":"e_1_3_2_17_2","doi-asserted-by":"publisher","unstructured":"Jason Gross Andres Erbsen Jade Philipoom Miraya Poddar-Agrawal and Adam Chlipala. 2022. Accelerating verified-compiler development with a verified rewriting engine. In Int\u2019l Conf. on Interactive Theorem Proving (ITP). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.17 doi:10.4230\/LIPIcs.ITP.2022.17","DOI":"10.4230\/LIPIcs.ITP.2022.17"},{"key":"e_1_3_2_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/1086642.1086644"},{"key":"e_1_3_2_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/3591286"},{"key":"e_1_3_2_20_2","unstructured":"David Kanter. 2016. RISC-V offers simple modular ISA: New CPU instruction set is open and extensible. Microprocessor Report (March 2016). https:\/\/riscv.org\/wp-content\/uploads\/2016\/04\/RISC-V-Offers-Simple-Modular-ISA.pdf"},{"key":"e_1_3_2_21_2","doi-asserted-by":"publisher","unstructured":"Andrew W. Keep and R. Kent Dybvig. 2013. A nanopass framework for commercial compiler development. In ACM SIGPLAN Conf. on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/2500365.2500618 doi:10.1145\/2500365.2500618","DOI":"10.1145\/2500365.2500618"},{"key":"e_1_3_2_22_2","doi-asserted-by":"publisher","unstructured":"Steven Keuchel and Tom Schrijvers. 2013. Generic datatypes \u00e0 la carte. In 9th ACM SIGPLAN Workshop on Generic Programming. https:\/\/doi.org\/10.1145\/2502488.2502491 doi:10.1145\/2502488.2502491","DOI":"10.1145\/2502488.2502491"},{"key":"e_1_3_2_23_2","doi-asserted-by":"publisher","DOI":"10.1145\/3649836"},{"key":"e_1_3_2_24_2","unstructured":"Lindsey Kuper. 2019. My first fifteen compilers. https:\/\/blog.sigplan.org\/2019\/07\/09\/my-first-fifteen-compilers"},{"key":"e_1_3_2_25_2","doi-asserted-by":"publisher","unstructured":"Chris Lattner Mehdi Amini Uday Bondhugula Albert Cohen Andy Davis Jacques Pienaar River Riddle Tatiana Shpeisman Nicolas Vasilache and Oleksandr Zinenko. 2021. MLIR: Scaling compiler infrastructure for domain specific computation. In Int\u2019l Symp. on Code Generation and Optimization (CGO). https:\/\/doi.org\/10.1109\/CGO51591.2021.9370308 doi:10.1109\/CGO51591.2021.9370308","DOI":"10.1109\/CGO51591.2021.9370308"},{"key":"e_1_3_2_26_2","volume-title":"Object-oriented programming in the BETA programming language","author":"Madsen Ole Lehrmann","year":"1993","unstructured":"Ole Lehrmann Madsen, Birger M\u00f8-Pedersen, and Kristen Nygaard. 1993. Object-oriented programming in the BETA programming language. Addison-Wesley."},{"key":"e_1_3_2_27_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-009-9155-4"},{"key":"e_1_3_2_28_2","doi-asserted-by":"publisher","unstructured":"Per Martin-L\u00f6f. 1982. Constructive mathematics and computer programming. In Logic Methodology and Philosophy of Science VI. Studies in Logic and the Foundations of Mathematics Vol. 104. https:\/\/doi.org\/10.1016\/S0049-237X(09)70189-2 doi:10.1016\/S0049-237X(09)70189-2","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"e_1_3_2_29_2","unstructured":"Dawn Michaelson Gopalan Nadathur and Eric Van Wyk. 2023. A modular approach to metatheoretic reasoning for extensible languages. arXiv:2312.14374 [cs.PL]. arXiv:2312.14374 doi:arXiv:2312.14374"},{"key":"e_1_3_2_30_2","unstructured":"Magnus O. Myreen. 2024. Much still to do in compiler verification (a perspective from the CakeML project). Keynote at the 45th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2024). Recording: https:\/\/www.youtube.com\/watch?v=eLFoHQgS6dA"},{"key":"e_1_3_2_31_2","volume-title":"Programming languages for scalable software extension and composition","author":"Nystrom Nathaniel","year":"2006","unstructured":"Nathaniel Nystrom. 2006. Programming languages for scalable software extension and composition. Ph.D. Dissertation. Cornell University. https:\/\/hdl.handle.net\/1813\/3726"},{"key":"e_1_3_2_32_2","doi-asserted-by":"publisher","unstructured":"Nathaniel Nystrom Stephen Chong and Andrew C. Myers. 2004. Scalable extensibility via nested inheritance. In ACM SIGPLAN Conf. on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1028976.1028986 doi:10.1145\/1028976.1028986","DOI":"10.1145\/1028976.1028986"},{"key":"e_1_3_2_33_2","doi-asserted-by":"publisher","unstructured":"Nathaniel Nystrom Michael R. Clarkson and Andrew C. Myers. 2003. Polyglot: an extensible compiler framework for Java. In Int\u2019l. Conf. on Compiler Construction (CC). https:\/\/doi.org\/10.1007\/3-540-36579-6_11 doi:10.1007\/3-540-36579-6_11","DOI":"10.1007\/3-540-36579-6_11"},{"key":"e_1_3_2_34_2","doi-asserted-by":"publisher","unstructured":"Nathaniel Nystrom Xin Qi and Andrew C. Myers. 2006. J&: nested intersection for scalable software composition. In ACM SIGPLAN Conf. on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1167473.1167476 doi:10.1145\/1167473.1167476","DOI":"10.1145\/1167473.1167476"},{"key":"e_1_3_2_35_2","doi-asserted-by":"publisher","unstructured":"Martin Odersky and Matthias Zenger. 2005. Scalable component abstractions. In ACM SIGPLAN Conf. on Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/1094811.1094815 doi:10.1145\/1094811.1094815","DOI":"10.1145\/1094811.1094815"},{"key":"e_1_3_2_36_2","doi-asserted-by":"publisher","DOI":"10.1145\/361598.361623"},{"key":"e_1_3_2_37_2","doi-asserted-by":"publisher","unstructured":"Dmitry Petrashko Ond\u0159ej Lhot\u00e1k and Martin Odersky. 2017. Miniphases: compilation using modular and efficient tree transformations. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3062341.3062346 doi:10.1145\/3062341.3062346","DOI":"10.1145\/3062341.3062346"},{"key":"e_1_3_2_38_2","unstructured":"Benjamin C. Pierce Arthur Azevedo de Amorim Chris Casinghino Marco Gaboardi Michael Greenberg C\u0103t\u0103lin Hri\u0163cu Vilhelm Sj\u00f6berg and Brent Yorgey. 2025. Software foundations: Volume 2 (programming language foundations). Version 6.8."},{"key":"e_1_3_2_39_2","doi-asserted-by":"publisher","unstructured":"Cl\u00e9ment Pit-Claudel Jade Philipoom Dustin Jamner Andres Erbsen and Adam Chlipala. 2022. Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3519939.3523706 doi:10.1145\/3519939.3523706","DOI":"10.1145\/3519939.3523706"},{"key":"e_1_3_2_40_2","unstructured":"Rocq. [n.d.]. The Rocq prover. https:\/\/rocq-prover.org"},{"key":"e_1_3_2_41_2","doi-asserted-by":"publisher","unstructured":"Dipanwita Sarkar Oscar Waddell and R. Kent Dybvig. 2004. A nanopass infrastructure for compiler education. In ACM SIGPLAN Conf. on Functional Programming (ICFP). https:\/\/doi.org\/10.1145\/1016850.1016878 doi:10.1145\/1016850.1016878","DOI":"10.1145\/1016850.1016878"},{"key":"e_1_3_2_42_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796805005605"},{"key":"e_1_3_2_43_2","doi-asserted-by":"publisher","unstructured":"Christopher Schwaab and Jeremy G. Siek. 2013. Modular type-safety proofs in Agda. In 7th Workshop on Programming Languages Meets Program Verification. https:\/\/doi.org\/10.1145\/2428116.2428120 doi:10.1145\/2428116.2428120","DOI":"10.1145\/2428116.2428120"},{"key":"e_1_3_2_44_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006758"},{"key":"e_1_3_2_45_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796818000229"},{"key":"e_1_3_2_46_2","doi-asserted-by":"publisher","unstructured":"Zachary Tatlock and Sorin Lerner. 2010. Bringing extensibility to verified compilers. In ACM SIGPLAN Conf. on Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/1806596.1806611 doi:10.1145\/1806596.1806611","DOI":"10.1145\/1806596.1806611"},{"key":"e_1_3_2_47_2","unstructured":"Philip Wadler et al. 1998. The expression problem. http:\/\/homepages.inf.ed.ac.uk\/wadler\/papers\/expression\/expression.txt Discussion on the Java-genericity mailing list."},{"key":"e_1_3_2_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/3133894"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729261","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:01:29Z","timestamp":1784196089000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729261"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":47,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729261"],"URL":"https:\/\/doi.org\/10.1145\/3729261","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}