{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/121675"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/121675","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Extracting and optimizing low-level bytecode from high-level verified Coq","abstract":"This document is an MEng thesis presenting MCQC, a compiler for extracting verified systems programs to low-level assembly, with no Runtime or Garbage Collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a series of memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions MCQC can generate executable code directly from Gallina and link it with trusted code, reducing the effort of implementing and executing verified systems.","abstract_html":"This document is an MEng thesis presenting MCQC, a compiler for extracting verified systems programs to low-level assembly, with no Runtime or Garbage Collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a series of memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions MCQC can generate executable code directly from Gallina and link it with trusted code, reducing the effort of implementing and executing verified systems.","abstract_has_math":false,"creators":["Ioannidis, Eleftherios Ioannis."],"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":["Frans Kaashoek and Nickolai Zeldovich."],"committee_chairs":[],"committee_members":[],"year":2019,"date_issued":"2019","date_published":"2019","updated_at":"2026-07-22T22:21:48Z","subjects":["Electrical Engineering and Computer Science."],"languages":["eng"],"rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"rights_urls":["http://dspace.mit.edu/handle/1721.1/7582"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/121675","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Frans Kaashoek and Nickolai Zeldovich."]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"]},{"key":"dc:contributor.other","label":"Dc Contributor Other","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."]},{"key":"dc:creator","label":"Author","values":["Ioannidis, Eleftherios Ioannis."]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2019-07-15T20:33:07Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2019-07-15T20:33:07Z"]},{"key":"dc:date.issued","label":"Date","values":["2019"]},{"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"]}]},{"id":"subjects_keywords","label":"Subjects and Keywords","entries":[{"key":"dc:subject","label":"Dc Subject","values":["Electrical Engineering and Computer Science."]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:language.iso","label":"Language (ISO)","values":["eng"]},{"key":"dc:rights","label":"Dc Rights","values":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."]},{"key":"dc:rights.uri","label":"Rights URI","values":["http://dspace.mit.edu/handle/1721.1/7582"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/121675"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description","label":"Description","values":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 51-53)."]},{"key":"dc:description.abstract","label":"Abstract","values":["This document is an MEng thesis presenting MCQC, a compiler for extracting verified systems programs to low-level assembly, with no Runtime or Garbage Collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a series of memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions MCQC can generate executable code directly from Gallina and link it with trusted code, reducing the effort of implementing and executing verified systems."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M. Eng."]},{"key":"dc:title","label":"Title","values":["Extracting and optimizing low-level bytecode from high-level verified Coq"]}]}],"canonical_facts":{"dc:contributor.advisor":["Frans Kaashoek and Nickolai Zeldovich."],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","EECS"],"dc:contributor.other":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science."],"dc:creator":["Ioannidis, Eleftherios Ioannis."],"dc:date.accessioned":["2019-07-15T20:33:07Z"],"dc:date.available":["2019-07-15T20:33:07Z"],"dc:date.issued":["2019"],"dc:description":["This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.","Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2019","Cataloged from student-submitted PDF version of thesis.","Includes bibliographical references (pages 51-53)."],"dc:description.abstract":["This document is an MEng thesis presenting MCQC, a compiler for extracting verified systems programs to low-level assembly, with no Runtime or Garbage Collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a series of memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions MCQC can generate executable code directly from Gallina and link it with trusted code, reducing the effort of implementing and executing verified systems."],"dc:description.degree":["M. Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/121675"],"dc:language.iso":["eng"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission."],"dc:rights.uri":["http://dspace.mit.edu/handle/1721.1/7582"],"dc:subject":["Electrical Engineering and Computer Science."],"dc:title":["Extracting and optimizing low-level bytecode from high-level verified Coq"],"dc:type":["Thesis"],"thesis:degree_name":["Master"]},"updated_at":"2026-07-22T22:21:48Z"}