Martin-Löf Type Theory

Martin-Löf Type Theory (MLTT) is a foundational system for constructive mathematics, equating propositions with types and proofs with programs.

Martin-Löf Type Theory (MLTT), also known as intuitionistic or constructive type theory, was developed by Per Martin-Löf starting in 1972. It provides an alternative foundation for mathematics, emphasizing constructivism: any existence proof must explicitly provide a 'witness' (e.g., a specific number for 'there exists a prime greater than 1000'). MLTT achieves this through the Curry-Howard isomorphism, where logical propositions correspond to types and proofs correspond to programs. This allows proofs to be treated as mathematical objects with computational content, enabling the creation of provably correct software in systems like Agda, Coq, and Idris. MLTT is characterized by dependent types, predicativity, and identity types, with both intensional and extensional variants.

https://ncatlab.org/nlab/show/Martin-L%C3%B6f+dependent+type+theory