Lambda the Ultimate

Johan Georg Granström studied intuitionistic type theory under Per Martin-Löf, who invented the subject. His PhD thesis is published by Springer and "combines philosophy, mathematical logic, and computer science".

Since May 2011, he works as software engineer for Google, where he has contributed to three major public launches and and submitted nine patent applications.

Johan is an active member of the academy: he has written three scientific papers; he is a reviewer for Zentralblatt MATH; he has delivered 25 public lectures; he represents Google in a FP7 EU grant application; and he is frequently consulted as a referee for Google scholarship applications, as well as external conference and journal publications.

Intuitionistic Type Theory.