[TYPES] Compiler correctness for a stack machine backend

[Anitha Gollamudi]

Thanks Matt, Xavier and Tobias for the suggestions.

Suppose that the IMP and the stack machines (given in these
references) are extended with an explicit heap and call stack as well
as instructions that operate on heap. Then, compiling addresses would
probably require an address-map that maps source heap addresses
(integers) to target heap addresses (integers). Is this reasonably standard?


On Tue, 29 Jun 2021 at 09:58, Tobias Nipkow <nipkow at in.tum.de> wrote:
>
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>
>
>
> 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/
> >>
>