Promising Compilation to ARMv8
Authors: Anton Podkopaev, Ori Lahav, Viktor Vafeiadis
ARMv8.3
A compilation correctness proof from the Promise machine to the axiomatic model ARMv8.3.
[Draft (In Russian), Full proof (In Russian)]
ARMv8 POP
A compilation correctness proof from the Promise machine to the operational model ARMv8 POP.
[Full paper, PLC slides, ECOOP slides]