Combining Small-Step and Big-Step Semantics to Verify Loop Optimizations

David Knothe, Oliver Bringmann

Verified compilers aim to guarantee that compilation preserves the observable behavior of source programs. While small-step semantics are widely used in such compilers, they are no…