Implementing and proving correctness of a call-by-push-value abstract machine
Author
Term
4. term
Education
Publication year
2024
Submitted on
2024-06-14
Pages
35
Abstract
Abstract machines are a cheap method of implementation, that offers better performance compared to interpreters, while being a tool to prove compiler correctness. This report presents the implementation and proof of correctness for a call-by-push-value abstract machine. The implemented abstract machine is based on the SECD machine, and was supported by the implementation of a call-by-push-value interpreter. We provide a proof of correctness using a bisimulation of the call-by-push-value semantics and the abstract machine's transition rules and configuration.
Documents