Implementing and proving correctness of a call-by-push-value abstract machine
Author
Hansen, Dion Sean
Term
4. term
Education
Publication year
2024
Pages
35
Abstract
Abstract machines are a low-cost way to implement programming languages. They can often run programs faster than interpreters and help show that compilers preserve program meaning. This report implements and proves correct an abstract machine for call-by-push-value (CBPV), an evaluation strategy that separates values from computations. The machine is based on the SECD machine, and we also implement a CBPV interpreter to support the design and provide a point of comparison. We prove correctness by establishing a bisimulation between the CBPV semantics and the machine's transition rules and configurations, showing a step-by-step correspondence.
Abstrakte maskiner er en billig måde at implementere programmeringssprog på. De kan ofte køre programmer hurtigere end fortolkere og hjælper med at bevise, at kompilatorer bevarer programmers betydning. Denne rapport implementerer og beviser korrektheden af en abstrakt maskine for call-by-push-value (CBPV), en evalueringsstrategi der adskiller værdier fra beregninger. Maskinen er baseret på SECD-maskinen. Vi implementerer også en CBPV-fortolker som støtte og sammenligningsgrundlag. Korrektheden vises med en bisimulation mellem CBPV's semantik og maskinens overgangsregler og konfigurationer, som etablerer skridt-for-skridt overensstemmelse.
[This apstract has been rewritten with the help of AI based on the project's original abstract]