I am a researcher at KTH Royal Institute of Technology in the Theoretical Computer Science division, primarily on topics related to program verification and proof engineering. I currently work in the Trustfull project towards trustworthy full-stack computing.
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 am an avid user of Coq for both proving and programming, usually complemented by a measure of OCaml. I also use HOL4 and other dialects in the ML family.