[ 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) Best Anitha [1]. https://cakeml.org/popl14.pdf [2]. https://xavierleroy.org/courses/EUTypes-2019/
