[TYPES] Compiler correctness for a stack machine backend

[Anitha Gollamudi]

Hi,

I am looking for references to  prove compilation correctness from
Imp/C-like language (preferably with pointers and function calls) to
a stack machine.

Using small-step/big-step semantics to prove compilation correctness
(à la Compcert) will be helpful. It need not be mechanised---a
pen-and-paper proof exposition works as well.

Here are a couple of references that are somewhat related to what I am
looking for.
(a) CakeML: Compiles ML to CakeML byetcode [1].
(b) Xavier Leroy's tutorial: It uses continuation-passing-style [2].

If you have other pointers, please suggest. (Lecture notes, if any,
are also helpful)

Best
Anitha


[1]. https://cakeml.org/popl14.pdf
[2]. https://xavierleroy.org/courses/EUTypes-2019/