Dear Haskell Cafe

I'm looking for information on past and current attempts to write semantics for Haskell.
Features I'm particularly interested in are:

• formal
• mechanised
• maintainable
• up to date

Of course, if nothing like that exists then partial attempts towards it could still be useful.

My ultimate aims include:

1. Make it viable to define Haskell formally (i.e. so mechanised semantics can take over the normative role of the Haskell reports).
   
2. Write a verified (or verify an existing) Haskell compiler (where verified means semantics preserving).

Cheers,
Ramana