I just recently completed my masters defence at DIKU, and my final thesis was mechanizing semantics for a contracts language using the Coq proof assistant and developing novel static analyses using abstract interpretation techniques.
The project
All the details can be found in the report here.