[TYPES] Compiler correctness for a stack machine backend

[Xavier Leroy]

On Sat, Jun 26, 2021 at 2:55 PM Anitha Gollamudi <anitha.gollamudi at gmail.com>
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)
>

The Jinja project (https://www.isa-afp.org/entries/Jinja.html) by Klein and
Nipkow contains a verified compiler for a sizable subset of Java to a
sizable subset of the Java VM.

Their textbook *Concrete Semantics* (http://concrete-semantics.org/) also
contains a proof of a much simpler compiler for IMP, similar in ambition to
my lecture notes [2], but with a different proof technique.

Hope this helps,

- Xavier Leroy



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