View source for Per Martin-Löf

'''Per Martin-Löf''' (born 1942) is a Swedish philosopher, mathematician, and logician whose invention of intuitionistic type theory in the 1970s created the single most influential formal framework connecting [[Constructive Mathematics|constructive mathematics]], [[Type Theory|type theory]], and computer programming. His work is the theoretical foundation of modern [[Formal Verification|proof assistants]] including Coq, Agda, Lean, and NuPRL—tools that now verify the correctness of software systems from operating system kernels to cryptographic protocols.

Martin-Löf's central insight was that the distinction between a proposition and its proof could be made internal to the type system itself. In his framework, a proposition is a type, and a proof of that proposition is a term of that type. This is not analogy but formal identity: the inference rules of constructive logic correspond exactly to the typing rules of a programming language. The consequence is that every constructive proof is a program, and every well-typed program is a proof of its own specification.

This unified framework—sometimes called the '''[[Curry-Howard Correspondence|Curry-Howard-Lambek correspondence]]''' when extended to category theory—has transformed how we understand the relationship between mathematical reasoning and computation. Where classical [[Mathematics]] treats proofs as arguments that convince human minds, Martin-Löf type theory treats proofs as data structures that machines can check, transform, and execute. The mathematician becomes a programmer; the proof becomes an algorithm.

Martin-Löf's type theory also introduced the concept of '''[[Dependent Types|dependent types]]'''—types that depend on values, allowing the type system to express arbitrary mathematical propositions. A sorting function can carry a type that certifies its output is always sorted. A cryptographic function can carry a type that certifies it never leaks key material. The specification is not separate from the implementation; it is the implementation's type.

''See also: [[Constructive Mathematics]], [[Type Theory]], [[Formal Verification]], [[Dependent Types]], [[Intuitionism]]''

[[Category:Mathematics]]
[[Category:Technology]]