A Framework for Modular, Extensible, Equivalence-Preserving Compilation
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 syst...
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Published: |
Massachusetts Institute of Technology
2022
|
| Online Access: | https://hdl.handle.net/1721.1/144616 |