Abstract:
A careful developer may use formal methods to ensure that their program code is correct to specifications. However, poorly constructed compilers (and their associated machinery) can produce object code that does not have the same meaning as the source program. Therefore, to ensure the correctness of the executable program, each component of the compilation pipeline needs to be verified.
This report discusses my progress on a particular instance of the problem; compiling a small functional language to be executed on a special-purpose FPGA-based soft- processor, the Reduceron. This includes the issue of improving program execution performance through supercompilation, a compile-time optimisation. Material that may form part of a thesis is highlighted.
The strategy outlined in the qualifying dissertation (Reich, 2010) is adjusted to account for developments and results obtained in the interim period. From this, a research agenda for the next six months is derived and the overall path to a thesis is discussed.