Proving Correctness of a Chez Scheme Compiler Pass
We present a proof of correctness for a pass of the Chez Scheme compiler over a subset of the Scheme programming language. To improve trust in our proof approach, we provide two different validation frameworks. The first, created with the Coq proof assistant, is a partial mechanization of the proof,...
| Main Author: | |
|---|---|
| Format: | Others |
| Published: |
DigitalCommons@CalPoly
2021
|
| Online Access: | https://digitalcommons.calpoly.edu/theses/2336 https://digitalcommons.calpoly.edu/cgi/viewcontent.cgi?article=3900&context=theses |