俺はコレ買ったけどね（ｗ　ちょっと痛い若気の至り
　Twenty-Five Years of Constructive Type Theory
　Proceedings of a Congress held in Venice, October 1995
　http://www.oup.com/us/catalog/general/subject/Mathematics/Logic/?view=usa&ci=0198501277

Description:
Per Martin-Lof's work on constructive type theory
has had a tremendous impact on logic and mathematics,
as well as important applications in computer science and linguistics.
This volume celebrates the birth of the subject and
provides an invaluable record of current activity.
It includes contributions from N. G. de Bruijn, William Tait, and Per Martin-Lof. Features

Features:
・Important paper by Martin-Lof published for the first time
・Unique record of last twenty-five years of the subject