Per Martin-Lof

Per Erik Rutger Martin-Lof (born 8 May 1942 in Stockholm) is a Swedish logician, philosopher and mathematical statistician whose work since the late 1970s has centered on logic. His development of intuitionistic type theory, a constructive foundation for mathematics introducing dependent types, has directly shaped computer science, influencing the calculus of constructions and the logical framework LF, and underlying proof systems including NuPRL, Lego, Rocq, Lean, ALF, Agda, Twelf, Epigram and Idris. He held a joint chair in mathematics and philosophy at Stockholm University until retiring in 2009, having received his PhD there in 1970 under Andrey Kolmogorov.