Verified compilation of a purely functional language to a realistic machine semanticsHrutvik Kanabar. PhD Thesis, University of Kent. 2023