From the tutorial's conclusion:<p>> The primary purpose of Morte is a proof-of-concept that a non-recursive calculus of constructions is the ideal system for the super-optimization of functional programs. Morte uses a simple, yet powerful, optimization scheme that consists entirely of normalizing terms using the ordinary reduction rules of lambda calculus. Morte emphasizes pushing optimization complexity out of the virtual machine and into the translation of abstractions to the calculus of constructions.