Patryk Zadarnowski. C, Lambda Calculus and Compiler Verification - a study in Haskell of purely-functional techniques for a formal specification of imperative programming languages and an epistemically-sound verification of their compilers. PhD thesis, University of New South Wales, Sydney, Australia, 2011. [doi]
Abstract is missing.