[ 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 <[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.
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/
