A modern elaboration of the ramified theory of types

DOI10.1007/BF00370835MaRDI QIDQ2563450zbMATH OpenFDO

Authors Twan Laan, Rob Nederpelt

Publication date 16 January 1997

Published in Studia Logica (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/BF00370835

zbMATH Keywords

lambda calculusPrincipia Mathematicaramified type theorytype system of Russell and Whiteheadtyped lambda calculus

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40)

Review text

The paper first formalizes the ramified type theory as (informally) described in the Principia Mathematica. This formalization is close to the ideas of the Principia, but also meets contemporary requirement on formality and accuracy, and therefore is a new supply to the known literature on the Principia. As an alternative, notions from the ramified type theory are expressed in a lambda calculus style. This situates the type system of Russell and Whitehead in a modern setting. Both formalizations are inspired by current developments in research on type theory and typed lambda calculus.

Recommendations

• Polymorphic type-checking for the ramified theory of types of \textit{Principia mathematica}
• scientific article; zbMATH DE number 2154397
• A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems
• scientific article; zbMATH DE number 2152246

Cites work

• A formulation of the simple theory of types
• Combinatory logic. Vol. II
• Combinatory logic. With two sections by William Craig.
• Comparison of Russell's resolution of the semantical antinomies with that of Tarski
• Foundations of set theory. With the collaboration of Dirk van Dalen. 2nd revised ed
• scientific article; zbMATH DE number 3873291 (Why is no real title available?)
• scientific article; zbMATH DE number 877752 (Why is no real title available?)
• scientific article; zbMATH DE number 3198017 (Why is no real title available?)
• Mathematics and Logic
• Outline of a Theory of Truth
• The foundations of mathematics. A study in the philosophy of science
• The lambda calculus. Its syntax and semantics. Rev. ed.

Cited in

(11)

• A modern perspective on type theory. From its origins until today
• Why ramify?
• The fact semantics for ramified type theory and the axiom of reducibility
• Types in Logic and Mathematics before 1940
• A relational formulation of the theory of types
• A constructive examination of a Russell-style ramified type theory
• scientific article; zbMATH DE number 2152246 (Why is no real title available?)
• scientific article; zbMATH DE number 2154397 (Why is no real title available?)
• scientific article; zbMATH DE number 877752 (Why is no real title available?)
• Polymorphic type-checking for the ramified theory of types of \textit{Principia mathematica}
• A correspondence between Martin-Löf type theory, the ramified theory of types and pure type systems

Describes a project that uses

Uses Software

• Mathematica
• Nuprl
• Automath

This page was built for publication: A modern elaboration of the ramified theory of types

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