By us:
A Principled Approach to Operating System Construction in Haskell
 Lennart Augustsson and Thomas Johnsson:
Parallel Graph Reduction with the <ν,G> machine
, FPCA 1989.
 Benjamin Gregoire and Xavier Leroy,
A compiled implementation of strong reduction
Formal certification of a compiler back-end, or: programming a compiler with a proof assistant