He studied intuitionistic type theory under Per Martin-Löf, who invented the subject. His PhD thesis is published by Springer under the title "Treatise on Intuitionistic Type Theory". Johan is an active member of the academy: he has published several books and scientific papers; he is a reviewer for Zentralblatt MATH; he is a member of the STL research unit; he has delivered dozens of public lectures; and he is frequently consulted as a referee, both internally at Google and for external conference and journal publications.