[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On Sat, Jun 26, 2021 at 2:55 PM Anitha Gollamudi <[email protected]> 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/ >
