Johan Georg Granström is a senior software engineer at Google Zürich, where he has contributed to several public launches and submitted over a dozen patent applications since joining Google in 2011. 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.