Automated type-checking for the ramiﬁed theory of types of the Principia Mathematica of Russell and Whitehead
This paper described a formal theory of type judgments for propositional logic notations of PM; I felt the need of my own automated type checker to check their examples. The type checker I wrote did indeed serve to help me referee the paper, but also took a rather diﬀerent approach to notation and typing for propositional functions of PM, which proved worth writing up independently in our own paper: Holmes, M. Randall, “Polymorphic type– checking for the ramiﬁed theory of types of Principia Mathematica”, in Fairouz Kamareddine, ed., Thirty–ﬁve Years of Automating Mathematics, Kluwer, 2003, pp. 173-215.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Polymorphic Type Checking for the Type Theory of the Principia Mathematica of Russell and Whitehead.M. Randall Holmes - unknown
The Triumph of Types: Principia Mathematica's Impact on Computer Science.Robert L. Constable - unknown
A Modern Elaboration of the Ramified Theory of Types.Twan Laan & Rob Nederpelt - 1996 - Studia Logica 57 (2-3):243 - 278.
Types in Logic and Mathematics Before 1940.Fairouz Kamareddine, Twan Laan & Rob Nederpelt - 2002 - Bulletin of Symbolic Logic 8 (2):185-245.
The Versatility of Universality inPrincipia Mathematica.Brice Halimi - 2011 - History and Philosophy of Logic 32 (3):241-264.
A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems.Fairouz Kamareddine & Twan Laan - 2001 - Journal of Logic, Language and Information 10 (3):375-402.
Russell's Substitutional Theory of Classes and Relations.Gregory Landini - 1987 - History and Philosophy of Logic 8 (2):171-200.
Leon Chwistek, The Principles of the Pure Type Theory , Translated by Adam Trybus with an Introductory Note by Bernard Linsky.Adam Trybus - 2012 - History and Philosophy of Logic 33 (4):329-352.
Quantification Theory in *9 of Principia Mathematica.Gregory Landini - 2000 - History and Philosophy of Logic 21 (1):57-77.
Nominalization, Predication and Type Containment.Fairouz Kamareddine & Ewan Klein - 1993 - Journal of Logic, Language and Information 2 (3):171-215.
Relations Vs Functions at the Foundations of Logic: Type-Theoretic Considerations.Paul Oppenheimer & Edward N. Zalta - 2011 - Journal of Logic and Computation 21:351-374.
A Note on Russell's Paradox in Locally Cartesian Closed Categories.Andrew M. Pitts & Paul Taylor - 1989 - Studia Logica 48 (3):377 - 387.
A New Interpretation of Russell's Multiple-Relation Theory of Judgment.Gregory Landini - 1991 - History and Philosophy of Logic 12 (1):37-69.
Added to index2010-12-22
Total downloads14 ( #329,667 of 2,158,237 )
Recent downloads (6 months)2 ( #194,705 of 2,158,237 )
How can I increase my downloads?