A modern perspective on type theory. From its origins until today (Q1887432)

This book presents a history of type theory, from Russell's early formulation (1908) to the present time. It explains also the framework of Pure Type Systems (PTSs), and shows for instance how the Ramified Type Theory from Principia Mathematica could be represented in this framework. It ends by some possible refinement of PTSs. For extra references on the history on propositions as types (part 2), one can point to \textit{J. P. Seldin}'s ``Curry's anticipation of the types used in programming languages'' [in: Proceedings of the Annual Meeting of the Canadian Society for History and Philosophy of Mathematics, Toronto, May 24--26, 2002, 148--163 (2002)], which shows that Curry anticipated the notion of dependent types, and to the forthcoming article of F. Cardone and R. Hindley.