Previous deforestation and supercompilation algorithms may introduce
accidental termination when applied to call-by-value programs. This hides
looping bugs from the programmer, and changes the behavior of a program
depending on whether it is optimized or not. We present a supercompilation
algorithm for a higher-order call-by-value language and prove that the
algorithm both terminates and preserves termination properties. This algorithm
utilizes strictness information to decide whether to substitute or not and
compares favorably with previous call-by-name transformations.