scientific article; zbMATH DE number 1062114

MaRDI QIDQ4354787zbMATH OpenFDO

Authors Twan Dismas Laurens Laan

Publication date 17 September 1997

zbMATH Keywords

Automathevolution of type theoryformal framework for type theories

Mathematics Subject Classification ID

Research exposition (monographs, survey articles) pertaining to mathematical logic and foundations (03-02) History of mathematical logic and foundations (03-03) Mechanization of proofs and logical operations (03B35) Second- and higher-order arithmetic and fragments (03F35)

Review text

Nowadays, type theory has many applications and is used in a lot of different disciplines. Even within logic and mathematics, there are a lot of different type systems. They serve several purposes, and are formulated in various ways. In this thesis we present a formal framework in which various type theories can be described. This framework is an extension of an already existing framework. For the development of this framework, we follow the evolution of type theory throughout the past century. However, we do not only give a mere historical description. On the contrary: our goal is not to describe the various type systems that have been developed in their historical setting, but to present them in a modern framework. In this way it becomes clear how the various type systems are related to each other, even if originally those systems are described in very different ways. Moreover, we can make clear what is the essence, or the common basis, of the various modern type theories. The historical line in this thesis is, therefore, only part of our method of research, and definitely not a goal of our research.

Recommendations

• History and philosophy of constructive type theory
• Type theory and formalisation of mathematics
• Publication:4204148
• A modern perspective on type theory. From its origins until today
• Logic in the 1930s: type theory and model theory
• scientific article; zbMATH DE number 1215502
• Mathematical logic: proof theory, type theory and constructive mathematics
• Higher-Order Logic and Type Theory
• Types in Logic and Mathematics before 1940
• scientific article; zbMATH DE number 1302061

Cited in

(4)

• Revisiting the notion of function
• A modern perspective on type theory. From its origins until today
• Proceeding in Abstraction. From Concepts to Types and the Recent Perspective on Information
• Automath and Pure Type Systems

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4354787)