A professor at University of Gothenburg influential in Type Theory Creations Calculus of Constructions Calculus of Inductive Constructions