Extracting and optimizing low-level bytecode from high-level verified Coq
This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2019
|
| Subjects: | |
| Online Access: | https://hdl.handle.net/1721.1/121675 |
| _version_ | 1826205640332148736 |
|---|---|
| author | Ioannidis, Eleftherios Ioannis. |
| author2 | Frans Kaashoek and Nickolai Zeldovich. |
| author_facet | Frans Kaashoek and Nickolai Zeldovich. Ioannidis, Eleftherios Ioannis. |
| author_sort | Ioannidis, Eleftherios Ioannis. |
| collection | MIT |
| description | This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. |
| first_indexed | 2024-09-23T13:16:35Z |
| format | Thesis |
| id | mit-1721.1/121675 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:16:35Z |
| publishDate | 2019 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1216752019-10-03T13:38:12Z Extracting and optimizing low-level bytecode from high-level verified Coq Ioannidis, Eleftherios Ioannis. Frans Kaashoek and Nickolai Zeldovich. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Electrical Engineering and Computer Science. 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). 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. by Eleftherios Ioannidis. M. Eng. M.Eng. Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science 2019-07-15T20:33:07Z 2019-07-15T20:33:07Z 2019 2019 Thesis https://hdl.handle.net/1721.1/121675 1102056840 eng 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. http://dspace.mit.edu/handle/1721.1/7582 53 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Ioannidis, Eleftherios Ioannis. Extracting and optimizing low-level bytecode from high-level verified Coq |
| title | Extracting and optimizing low-level bytecode from high-level verified Coq |
| title_full | Extracting and optimizing low-level bytecode from high-level verified Coq |
| title_fullStr | Extracting and optimizing low-level bytecode from high-level verified Coq |
| title_full_unstemmed | Extracting and optimizing low-level bytecode from high-level verified Coq |
| title_short | Extracting and optimizing low-level bytecode from high-level verified Coq |
| title_sort | extracting and optimizing low level bytecode from high level verified coq |
| topic | Electrical Engineering and Computer Science. |
| url | https://hdl.handle.net/1721.1/121675 |
| work_keys_str_mv | AT ioannidiseleftheriosioannis extractingandoptimizinglowlevelbytecodefromhighlevelverifiedcoq |