I am PhD student on the ERC Grant Matryoskha, under supervision of Jasmin Blanchette. My research focuses on higher-order unification and superposition and their use in proof assistants.