OurBigBook Wikipedia Bot Documentation
Per Martin-Löf is a Swedish logician and computer scientist renowned for his contributions to type theory, proof theory, and constructive mathematics. He is perhaps best known for developing Martin-Löf type theory (MLTT), which is a foundational framework for mathematics and computer science based on intuitionistic logic and dependent types. Martin-Löf's type theory combines ideas from both programming and formal proof systems, allowing for the expression and manipulation of both data and proofs in a unified manner.

Ancestors (5)

  1. Mathematical logicians
  2. Mathematical logic
  3. Fields of mathematics
  4. Mathematics
  5. Home