Martin-Lof Type Theory

Martin-Lof Type Theory is a programming language created in 1972 by Per Martin-Löf.

Martin-Löf Type Theory (MLTT) is a formal system developed by Per Martin-Löf for constructive mathematics, combining typed lambda calculus with dependent types and the Curry-Howard correspondence. It serves as a foundation for proof assistants and functional programming languages, emphasizing constructive proofs as programs.

• Tags: programming language, mathematics
• Early development of Martin-Lof Type Theory happened in University of Stockholm
• Automath and Lambda Calculus influenced the design of Martin-Lof Type Theory