Certified compiler and optimizations in Coq/Agda I am interested in verified compilers formalized in Martin-Löf type theory, i.e. Coq/Agda. At the moment I’ve 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.
this paper by Yves Bertot, Benjamin Gr´egoire, and Xavier Leroy builds an optimizing compiler for a C-like language based purely on the Coq specification.  some of this technology is apparently utilized in the CompCert C compiler.

A structured approach to proving compiler
optimizations based on dataflow analysis

it considers the correctness of two optimizations, constant propagation (CP) and common subexpression elimination (CSE), section 4. these optimizations are more advanced than those that are associated with the non Coq-based compiler(s) for the same language. see eg this benchmark chart compared to gcc. (the Coq-based compiler is presumably slower to compile although this is rarely mentioned!) 


  An original aspect of ConCert is that most of the compiler is written directly
  in the Coq specification language, in a purely functional style. The executable
  compiler is obtained by automatic extraction of Caml code from this specification.


however at the end of the paper they do note that there are some compiler optimizations in real compilers that cant be modelled in their framework.

improved optimization is not the only element of consideration here, another aspect is that compiler optimization logic can be subject to subtle defects esp due to its complex nature. over the years gcc has been found to have bugs in its numerous optimization logic routines. eg gcc bug?