I am interested in verified compilers formalized in Martin-Lf type theory, i.e. Coq/Agda. At the moment Ive written a small toy example. Therewith I can prove that my optimizations are correct. For example that additions with zero can be eliminated, i.e. expressions like x + 0.Are there optimizations that are difficult to perform with a regular compiler, that would serve as a good example? Is it possible to prove certain properties of a program that allow optimizations that are not possible to perform with a regular compiler? (i.e. without the inference that is possible with a theorem prover)I would be interested in ideas or examples and also references on the topic.A related question:Compiler correctness proofs edit:As Tsuyoshi nicely put it in the comments:I am looking for optimization techniques which are difficult to implement if a compiler is written in (say) C but easier to implement if a compiler is written in (say) Coq. As Agda compiles to C (via haskell) it is possible to do everything that is possible in Agda also in C. Probably the only benefit of theorem provers like Coq/Agda is that the compiler and the optimizations can be verified.edit2:As suggested by Vijay D I write what I've read so far.I mainly focused on Xavier Leroy and the CompCert project at INRIA (there is a 80 pages paper that is a good read, I think).A second interest was in the work of Anton Setzer on interactive programs. I though that perhaps his work could be used to prove properties about IO programs and bisimulation of IO programs. Thanks for mentioning Sewell. I've heard his talk Tales from the jungle at ICFP and read perhaps 2-3 of his papers. But I haven't specifically looked at his work and that of his coauthors.I did not yet find out where to start or look for papers on optimizing compilers; e.g., which optimizations would be interesting to look at in the setting of a verified compiler. 
Certified compiler and optimizations in Coq/Agda
reference request;pl.programming languages;type theory;semantics;compilers