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]