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-L6f 's type theory. This work has made an important contribution to the fields of logic and the foundationsof 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.
The conference "Twenty-five years of constructivetype theory" took place in Venice, 19-21 October 1995. It originated from a desire to celebrate the anniversary by gath- ering together those people who have worked or are still working on type theory and related topics.