A master thesis from Aalborg University
Implementing and proving correctness of a call-by-push-value abstract machine
Author(s)
Term
4. term
Education
Publication year
2024
Submitted on
2024-06-14
Pages
35 pages
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
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.