Twenty Five Years of Constructive Type Theory

Martin-Lf Type Theory is both an important and practical formalization and a focus for a charismatic view of the foundations of mathematics. Per Martin-Lf's work has been of huge significance in the fields of logic and the foundations of mathematics, and has important applications in areas such as computing science and linguistics. This volume celebrates the twenty-fifth anniversary of the birth of the subject, and is an invaluable record both of areas of current activity and of the early development of the subject. Also published for the first time is one of Per Martin-Lf's earliest papers.