Polymorphic type checking for the type theory of the Principia Mathematica of Russell and

This is a brief report on results reported at length in our paper [2], made for the purpose of a presentation at the workshop to be held in November 2011 in Cambridge on the Principia Mathematica of Russell and Whitehead ([?], hereinafter referred to briefly as PM). That paper grew out of a reading of the paper [3] of Kamareddine, Nederpelt, and Laan. We refereed this paper and found it useful for checking their examples to write our own independent computer type-checker for the type system of PM ([1]), which led us to think carefully about formalization of the language and the type system of PM A modern mathematical logician reading PM finds that it is not completely formalized in a modern sense. The type theory in particular is inarguably not formalized, as no notation for types is given at all! In PM itself, the only type annotations which appear are occasional numerical indices indicating order; the type notation we use here extends one introduced later by Ramsey. The authors of PM regard the absence of explicit indications of type as a virtue of thei