[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
On 6/24/2021 19:21, Anitha Gollamudi 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)
Hello Anitha, Perhaps the following may also be of use: https://github.com/MattPD/cpplinks/blob/master/compilers.correctness.md Best, Matt
