References

[5] Xavier Leroy: Formal certification of a compiler back-end, or: programming a compiler with a proof assistant, POPL 2006.