[TYPES] Compiler correctness for a stack machine backend

[Matt P. Dziubinski]

On 6/24/2021 19:21, Anitha Gollamudi wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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)

Hello Anitha,

Perhaps the following may also be of use:

https://github.com/MattPD/cpplinks/blob/master/compilers.correctness.md

Best,
Matt