Per Martin-Löf

Per Erik Rutger Martin-Löf (born 1942) is a Swedish logician, philosopher, and mathematician. He is best known for developing intuitionistic type theory as a constructive foundation of mathematics. Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University. He is the brother of Anders Martin-Löf. In 1964–65 Martin-Löf was studying under the supervision of Kolmogorov in Moscow, refining the notion of a random sequenc... more

Per Erik Rutger Martin-Löf (born 1942) is a Swedish logician, philosopher, and mathematician. He is best known for developing intuitionistic type theory as a constructive foundation of mathematics. Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University. He is the brother of Anders Martin-Löf. In 1964–65 Martin-Löf was studying under the supervision of Kolmogorov in Moscow, refining the notion of a random sequence. During this time he wrote his frequently cited article On the definition of random sequences. From 1968 to '69 he worked as an Assistant Professor at the University of Chicago where he met William Alvin Howard with whom he discussed issues related to the Curry-Howard correspondence. Martin-Löf's first draft article on type theory dates back to 1971. This impredicative theory generalized Girard's System F. However, this system turned out to be inconsistent due to Girard's paradox which was discovered by Girard when studying System U, an... less