Automated type-checking for the ramiﬁed theory of types of the Principia Mathematica of Russell and Whitehead
Graduate studies at Western
|Abstract||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)|
|Through your library||Only published papers are available at libraries|
Similar books and articles
M. Randall Holmes, Polymorphic Type Checking for the Type Theory of the Principia Mathematica of Russell and Whitehead.
Twan Laan & Rob Nederpelt (1996). A Modern Elaboration of the Ramified Theory of Types. Studia Logica 57 (2-3):243 - 278.
Fairouz Kamareddine, Twan Laan & Rob Nederpelt (2002). Types in Logic and Mathematics Before 1940. Bulletin of Symbolic Logic 8 (2):185-245.
Brice Halimi (2011). The Versatility of Universality inPrincipia Mathematica. History and Philosophy of Logic 32 (3):241-264.
Fairouz Kamareddine & Twan Laan (2001). A Correspondence Between Martin-Löf Type Theory, the Ramified Theory of Types and Pure Type Systems. Journal of Logic, Language and Information 10 (3):375-402.
Gregory Landini (1987). Russell's Substitutional Theory of Classes and Relations. History and Philosophy of Logic 8 (2):171-200.
Adam Trybus (2012). Leon Chwistek, The Principles of the Pure Type Theory (1922), Translated by Adam Trybus with an Introductory Note by Bernard Linsky. History and Philosophy of Logic 33 (4):329-352.
Gregory Landini (2000). Quantification Theory in *9 of Principia Mathematica. History and Philosophy of Logic 21 (1):57-77.
Dermot Cassidy (2007). Russell's Divine Ancestors. History and Philosophy of Logic 28 (2):123-132.
Fairouz Kamareddine & Ewan Klein (1993). Nominalization, Predication and Type Containment. Journal of Logic, Language and Information 2 (3):171-215.
Paul Oppenheimer & Edward N. Zalta (2011). Relations Vs Functions at the Foundations of Logic: Type-Theoretic Considerations. Journal of Logic and Computation 21:351-374.
Andrew M. Pitts & Paul Taylor (1989). A Note on Russell's Paradox in Locally Cartesian Closed Categories. Studia Logica 48 (3):377 - 387.
Gregory Landini (1991). A New Interpretation of Russell's Multiple-Relation Theory of Judgment. History and Philosophy of Logic 12 (1):37-69.
Added to index2010-12-22
Total downloads5 ( #170,097 of 739,325 )
Recent downloads (6 months)2 ( #37,029 of 739,325 )
How can I increase my downloads?