About me

I am a researcher and teacher at KTH Royal Institute of Technology in the Department of Theoretical Computer Science and the STEP research group. I do research primarily on topics related to program verification and proof engineering.

Research interests

I am interested in development of techniques and tools based on proof assistants for construction of functionally correct and secure software systems; see my research publications on DBLP and Google Scholar. I use Rocq for both proving and programming and am a member of the Rocq Team, where I help maintain the Rocq opam archive, the Rocq Platform, and Rocq-community. I also use HOL4 and usually program in languages in the ML family such as OCaml, Standard ML, and CakeML.