Yiming Xu's 2019 honours thesis in mathematics, on "Formalizing Modal Logic in HOL", supervised by Scott Morrison, is available as

• the submitted thesis and a
• git repository of the HOL code

---