A modern perspective on type theory. From its origins until today
type: Item
instance of: scholarly article
title: A modern perspective on type theory. From its origins until today
zbMATH Open document ID: 1077.03006
author: Fairouz Kamareddine
author: Twan Laan
author: Rob Nederpelt
published in: Applied Logic Series
publication date: 2004-11-25T00:00:00Z
review text: 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.
reviewed by: Thierry Coquand
Mathematics Subject Classification ID: 03B15
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 03-03
Mathematics Subject Classification ID: 03B35
Mathematics Subject Classification ID: 03B40
Mathematics Subject Classification ID: 68N18
zbMATH DE Number: 2119068
zbMATH Keywords: \(\lambda\)-calculus
zbMATH Keywords: type systems
MaRDI profile type: Publication
Recommended article: A modern elaboration of the ramified theory of types
Recommended article: Q4354787
Recommended article: Q4247306
Recommended article: A modular construction of type theories
Recommended article: History and philosophy of constructive type theory
Recommended article: Type theory and formal proof. An introduction
Recommended article: Q4461714
Recommended article: Q4724604
Recommended article: Introduction to Type Theory
Recommended article: In the Search of a Naive Type Theory
description: scientific article; zbMATH DE number 2119068