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