Certified optimizer
This optimizer was initially designed for the backend of the Albert compiler, it has been slightly generalized and certified. The main theorem is the last one in file typed_optimizer.v:
If the untyped instruction sequence i can be typechecked from stack type A to stack type B and then run successfully on stack sA, then (optimizer.optimize i) can also be typechecked from stack type A to stack type B and run successfully on stack sA yielding the same result.