All Topics  
Per Martin-Löf

 
Per Martin Löf

 
   Email Print
   Bookmark   Link
 

 

Per Martin-Löf
 
 
  Topics Per Martin-Löf Topic Home

Per Erik Rutger Martin-Löf (born 1942) is a Swedish
Sweden

Sweden , officially the Kingdom of Sweden , is a Nordic countries on the Scandinavian Peninsula in Northern Europe. Sweden has land borders with Norway to the west and Finland to the northeast, and it is connected to Denmark by the ?resund Bridge in the south....
 logician, philosopher, and mathematician
Mathematician

A mathematician is a person whose primary area of study and/or research is the field of mathematics....
. He is best known for developing intuitionistic type theory
Intuitionistic type theory

Intuitionistic type theory, or constructive type theory, or Martin-L?f type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism....
 as a constructive foundation of mathematics. Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University
Stockholm University

Stockholm University is a state university in Stockholm, Sweden. It has about 27,500 students studying at four faculties....
. He is the brother of Anders Martin-Löf
Anders Martin-Löf

Anders Martin-L?f , born 1940, is a Sweden physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
.

In 1964–65 Martin-Löf was studying under the supervision of Kolmogorov in Moscow, refining the notion of a random sequence
Random sequence

A random sequence is a kind of stochastic process. In short, a random sequence is a sequence of random variables.Random sequences are essential in statistics....
.






Discussion
Ask a question about 'Per Martin-Löf'
Start a new discussion about 'Per Martin-Löf'
Answer questions from other users
Full Discussion Forum



Encyclopedia


Per Martinloef
Per Erik Rutger Martin-Löf (born 1942) is a Swedish
Sweden

Sweden , officially the Kingdom of Sweden , is a Nordic countries on the Scandinavian Peninsula in Northern Europe. Sweden has land borders with Norway to the west and Finland to the northeast, and it is connected to Denmark by the ?resund Bridge in the south....
 logician, philosopher, and mathematician
Mathematician

A mathematician is a person whose primary area of study and/or research is the field of mathematics....
. He is best known for developing intuitionistic type theory
Intuitionistic type theory

Intuitionistic type theory, or constructive type theory, or Martin-L?f type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism....
 as a constructive foundation of mathematics. Per Martin-Löf holds a joint chair for Mathematics and Philosophy at Stockholm University
Stockholm University

Stockholm University is a state university in Stockholm, Sweden. It has about 27,500 students studying at four faculties....
. He is the brother of Anders Martin-Löf
Anders Martin-Löf

Anders Martin-L?f , born 1940, is a Sweden physicist and mathematician. He is a professor in insurance mathematics and mathematical statistics since 1987 at the Department of Mathematics of Stockholm University....
.

In 1964–65 Martin-Löf was studying under the supervision of Kolmogorov in Moscow, refining the notion of a random sequence
Random sequence

A random sequence is a kind of stochastic process. In short, a random sequence is a sequence of random variables.Random sequences are essential in statistics....
. 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
University of Chicago

The University of Chicago is a private university located principally in the Hyde Park, Chicago neighborhood of Chicago. Although an older university by the same name existed prior to its founding, the modern University of Chicago credits its founding to the oil magnate John D....
 where he met William Alvin Howard
William Alvin Howard

William Alvin Howard is a proof theorist best-known for his work demonstrating formal similarity between intuitionistic logic and the simply typed lambda calculus that has come to be known as the Curry-Howard correspondence....
 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
Impredicative

In mathematics and logic, impredicativity is the property of a self reference definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined....
 theory generalized Girard's
Jean-Yves Girard

Jean-Yves Girard is a France logician working in proof theory. His contributions include a proof of strong normalization in a system of second-order logic called system F; the invention of linear logic; the geometry of interaction; and ludics....
 System F
System F

System F, also known as the polymorphic lambda calculus or the second-order lambda calculus, is a typed lambda calculus. It was discovered independently by the logician Jean-Yves Girard and the computer scientist John C....
. However, this system turned out to be inconsistent
Consistency proof

In logic, a consistent theory is one that does not contain a contradiction. The lack of contradiction can be defined in either semantic or syntactic terms....
 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
Intuitionistic type theory

Intuitionistic type theory, or constructive type theory, or Martin-L?f type theory or just Type Theory is a logical system and a set theory based on the principles of mathematical constructivism....
, his meaning explanation, a form of proof-theoretic semantics
Proof-theoretic semantics

Proof-theoretic semantics is an approach to the Formal semantics that attempts to locate the meaning of propositions and logical connectives not in terms of interpretations, as in Tarskian approaches to semantics, but in the role that the proposition or logical connective plays within the system of inference....
, which justifies predicative
Impredicative

In mathematics and logic, impredicativity is the property of a self reference definition. More precisely, a definition is said to be impredicative if it invokes the set being defined, or another set which contains the thing being defined....
 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 type
Dependent type

In computer science and logic, a dependent type is a type which depends on a value. Dependent types play a central role in intuitionistic type theory and in the design of experimental functional programming languages like Dependent ML and Epigram ....
s and directly influenced the development of the calculus of constructions
Calculus of constructions

The calculus of constructions is a higher-order typed lambda calculus, initially developed by Thierry Coquand, where Data types are first-class values....
 and the logical framework LF
LF (logical framework)

In type theory, the LF logical framework provides a means to define logics. It is based on a general treatment of syntax, rules and proofs by means of a dependent type theory lambda calculus....
. A number of popular computer-based proof systems are based on type theory, for example NuPRL
NuPRL

NuPRL is a higher-order proof development system developed at Cornell University. It was founded by Joseph L. Bates and Robert L. Constable in 1979 and, since then, many have contributed to the development of NuPRL....
, LEGO, Coq
Coq

In computer science, Coq is a proof assistant application. It allows the expression of mathematics assertions, mechanically checks proofs of these assertions, helps to find formal proofs, and extracts a certified program from the constructive proof of its formal specification....
, ALF, Agda
Agda theorem prover

Agda is a proof assistant, i.e. a computer program that can check mathematical proofs. More specifically, it is an Interactive theorem proving for developing constructive proofs in a variant of Per Martin-L?f's Intuitionistic Type Theory....
, Twelf
Twelf

Twelf is an implementation of the logical framework LF . It is used for logic programming and for the formalization of programming language theory....
 and Epigram.