 Intuitionistic type theory

Intuitionistic Type Theory (ITT) is a branch of mathematical logic and a formal system that combines elements of type theory with intuitionistic logic. It was developed in the late 20th century, particularly through the work of mathematicians and computer scientists like Per Martin-Löf. ITT is significant in both the foundations of mathematics and in the study of programming languages and proof assistants.