[TYPES] Compiler correctness for a stack machine backend

[Tobias Nipkow]

On 26/06/2021 17:21, Xavier Leroy wrote:
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> 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.

Recently a shorter proof of the same material was published online:

https://www.isa-afp.org/entries/IMP_Compiler.html

Best
Tobias

> Hope this helps,
> 
> - Xavier Leroy
> 
> 
> 
>>
>> Best
>> Anitha
>>
>>
>> [1]. https://cakeml.org/popl14.pdf
>> [2]. https://xavierleroy.org/courses/EUTypes-2019/
>>