|
 |
|
|||||||||||
|
|
|
|
|||||||||||
|
|
A Simple Supercompiler Formally Verified in Coq Dimitur Krustev,
We study an approach for verifying the correctness of a simplified supercompiler in Coq. While existing supercompilers are not very big in size, they combine many different program transformations in intricate ways, so checking the correctness of their implementation poses challenges. The presented method relies on two important technical features to achieve a compact and modular formalization: first, a very limited object language; second, decomposing the supercompilation process into many sub-transformations, whose correctness can be checked independently. In particular, we give separate correctness proofs for two key parts of driving - normalization and positive information propagation - in the context of a non-Turing-complete expression sub-language. Though our supercompiler is currently limited, its formal correctness proof can give ideas for verifying more realistic implementations.
|
