Correctness of the TRIM Compiler
The goal of the 1996 doctoral thesis of Lutz Hamel at Oxford University was produce a provably correct compiler for order sorted term rewriting. The target of this compiler was the TRIM abstract machine, and an algebraic framework was used for the correctness proof, based on equational specifications for the syntax and semantics of both the source and target languages. Correctness is proved by showing that the source semantics is preserved by the translation (compilation) into the target semantics. The compiler was implemented in C++ and actually produces quite efficient code.

The style of this example is rather informal, in that complete logical rigor was neither attempted nor achieved. In particular, some of the lemmas only have intuitive explanations, not formal proofs. We view this as an advantage for the purpose of illustrating our approach, because it shows that we can support industrial style proofs, where it is not regarded as economically worthwhile to achieve full formality.

To the first tatami (i.e., proof page) of the of proof the corrextness for the TRIM compiler.
To the Tatami hand made demos homepage.
To the Links Project homepage.
to the UCSD Meaning and Computation Lab homepage.
15 February 1998