{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/144616"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/144616","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"A Framework for Modular, Extensible, Equivalence-Preserving Compilation","abstract":"I present Pyrosome1 , a generic framework for the verification of extensible, compositional compilers in Coq. Current techniques for proving compiler correctness are generally tied to the specific structures of the languages and compilers that they support. This limits the extent to which these systems can be extended and composed. In Pyrosome, verified compilers are fully extensible, meaning that to add a new feature to a language simply requires defining and verifying the compilation of that single feature, reusing the old correctness theorem to cover all other cases. This is made possible by an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. My work supports vertical composition of any compilers expressed in Pyrosome in addition to feature extension. Since my design requires compilers to support open programs, my correctness guarantees support linking with any target code of the appropriate type. As a case study, I present a multipass compiler from STLC through CPS translation and closure conversion, and show that natural numbers, the unit type, recursive functions, and a global heap can be added to this compiler while reusing the original proofs.","abstract_html":"I present Pyrosome1 , a generic framework for the verification of extensible, compositional compilers in Coq. Current techniques for proving compiler correctness are generally tied to the specific structures of the languages and compilers that they support. This limits the extent to which these systems can be extended and composed. In Pyrosome, verified compilers are fully extensible, meaning that to add a new feature to a language simply requires defining and verifying the compilation of that single feature, reusing the old correctness theorem to cover all other cases. This is made possible by an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. My work supports vertical composition of any compilers expressed in Pyrosome in addition to feature extension. Since my design requires compilers to support open programs, my correctness guarantees support linking with any target code of the appropriate type. As a case study, I present a multipass compiler from STLC through CPS translation and closure conversion, and show that natural numbers, the unit type, recursive functions, and a global heap can be added to this compiler while reusing the original proofs.","abstract_has_math":false,"creators":["Jamner, Dustin"],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Chlipala, Adam"],"committee_chairs":[],"committee_members":[],"year":2022,"date_issued":"2022-05","date_published":"2022-05","updated_at":"2026-07-22T22:21:16Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"rights_urls":["http://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/144616","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Chlipala, Adam"]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"]},{"key":"dc:creator","label":"Author","values":["Jamner, Dustin"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2022-08-29T15:59:49Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2022-08-29T15:59:49Z"]},{"key":"dc:date.issued","label":"Date","values":["2022-05"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master","Master of Science in Electrical Engineering and Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright MIT"]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/144616"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["I present Pyrosome1 , a generic framework for the verification of extensible, compositional compilers in Coq. Current techniques for proving compiler correctness are generally tied to the specific structures of the languages and compilers that they support. This limits the extent to which these systems can be extended and composed. In Pyrosome, verified compilers are fully extensible, meaning that to add a new feature to a language simply requires defining and verifying the compilation of that single feature, reusing the old correctness theorem to cover all other cases. This is made possible by an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. My work supports vertical composition of any compilers expressed in Pyrosome in addition to feature extension. Since my design requires compilers to support open programs, my correctness guarantees support linking with any target code of the appropriate type. As a case study, I present a multipass compiler from STLC through CPS translation and closure conversion, and show that natural numbers, the unit type, recursive functions, and a global heap can be added to this compiler while reusing the original proofs."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["S.M."]},{"key":"dc:title","label":"Title","values":["A Framework for Modular, Extensible, Equivalence-Preserving Compilation"]}]}],"canonical_facts":{"dc:contributor.advisor":["Chlipala, Adam"],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"],"dc:creator":["Jamner, Dustin"],"dc:date.accessioned":["2022-08-29T15:59:49Z"],"dc:date.available":["2022-08-29T15:59:49Z"],"dc:date.issued":["2022-05"],"dc:description.abstract":["I present Pyrosome1 , a generic framework for the verification of extensible, compositional compilers in Coq. Current techniques for proving compiler correctness are generally tied to the specific structures of the languages and compilers that they support. This limits the extent to which these systems can be extended and composed. In Pyrosome, verified compilers are fully extensible, meaning that to add a new feature to a language simply requires defining and verifying the compilation of that single feature, reusing the old correctness theorem to cover all other cases. This is made possible by an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by sorted equational theories, so all compiler-correctness proofs boil down to type-checking and equational reasoning. My work supports vertical composition of any compilers expressed in Pyrosome in addition to feature extension. Since my design requires compilers to support open programs, my correctness guarantees support linking with any target code of the appropriate type. As a case study, I present a multipass compiler from STLC through CPS translation and closure conversion, and show that natural numbers, the unit type, recursive functions, and a global heap can be added to this compiler while reusing the original proofs."],"dc:description.degree":["S.M."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/144616"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright MIT"],"dc:rights.uri":["http://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["A Framework for Modular, Extensible, Equivalence-Preserving Compilation"],"dc:type":["Thesis"],"thesis:degree_name":["Master","Master of Science in Electrical Engineering and Computer Science"]},"updated_at":"2026-07-22T22:21:16Z"}