From Wikipedia, the free encyclopedia

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 inconsistent extension of System F. This experience led Per Martin-Löf to develop the philosophical foundations of type theory, his meaning explanation, a form of proof-theoretic semantics, which justifies predicative type theory as presented in his 1984 Bibliopolis book, and extended in a number of increasingly philosophical texts, such as his influential On the Meanings of the Logical Constants and the Justifications of the Logical Laws.

The 1984 type theory was extensional while the type theory presented in the book by Nordström et al. in 1990, which was heavily influenced by his later ideas, was intensional and more amenable to being implemented on a computer.

Martin-Löf's intuitionistic type theory developed the notion of dependent types and directly influenced the development of the calculus of constructions and the logical framework LF. A number of popular computer-based proof systems are based on type theory, for example NuPRL, LEGO, Coq, ALF, Agda, Twelf and Epigram.

[edit] References

• Per Martin-Löf. "The Definition of Random Sequences." Information and Control, 9(6): 602-619, 1966.
• Per Martin-Löf. Intuitionistic type theory. Napoli, Bibliopolis, 1984.
• Bengt Nordström, Kent Petersson, and Jan M. Smith. Programming in Martin-Löf's Type Theory. Oxford University Press, 1990. (The book is out of print, but a free version has been made available.)
• Per Martin-Löf. "On the Meanings of the Logical Constants and the Justifications of the Logical Laws." Nordic Journal of Philosophical Logic, 1(1): 11-60, 1996.