Tail Recursion Modulo Cons Optimization in CakeML

Abstract

In this project, the Tail Recursion Modulo Cons (TMC) optimization is implemented in the end-to-end verified CakeML compiler. The optimization makes tail recursive those functions which contain a recursive call nested inside one or more constructors. The TMC transformation is applied in the bytecode-value intermediate language (BVI) and rewrites functions in a way that cannot be done manually in CakeML source code. The syntax and semantics of BVI are extended with three new language constructs, and a new compiler phase is added to rewrite BVI programs using the new constructs. The compiler is implemented and formally verified in the HOL4 interactive theorem prover, and included in the project is a mechanized proof that the transformation produces code that is semantically equivalent to the original.