In lectures and a series of papers, beginning in 1970, Per Martin-L6f has developed a constructive foundation of mathematics, which he called intuitionistic type theory and which has come to be known as Martin-Lof's type theory. This work has made animportant contribution to the fields of logic and the foundations of mathematics and is also of broader philosophical significance. Its depth and relevance can be seen by its increasing application to a variety of fields from computing science to linguistics.