As can probably be discerned from the list of speakers, this meeting was intended to address a broad range of interests: history, foundational mathematics, philosophy, type theory and mechanical theorem-proving. The organisers hoped that the symposium would be valuable to people interested in the intersection of these areas, or in relevant sub-branches of each area, and that practitioners and students alike would benefit from attending this meeting.

The redacted delegate list can be downloaded here.

The organisers thank the following for their financial or organisational help: Archive for Mathematical Sciences & Philosophy; Ms Shirley Bidgood; British Logic Colloquium; British Society for the Philosophy of Science; Cambridge University Press; Computer Laboratory, Cambridge; Prof. Neil Dodgson; Mr Hiro Funakoshi; Ms Tanya Hall; Mr Tim Hennock; Dr Sean Holden; Morgan Phoa Family Fund; Microsoft Research; Ms Carol Nightingale; Dr Arthur Norman; Prof. Hugh Osborn; Student-Run Computing Facility; Trinity College; Trinity Mathematical Society; Mr Michael Wright; Mr Edward Yang.

Set theory began to be developed on a large scale from the late 1890s onwards; for example, it was part of the mathematical logic that grounded logicism, and for convenience much of Principia mathematica was elaborated in its terms. Several different parts and features of set theory became prominent, and logicism was supposed to embrace all of them. In practice, though, how many did it tackle?
Download timeline and summary.

I intend to stress the theme that programming languages, starting with Algol 60, introduced a notion of type related to PM that has steadily worked its way deep into the design philosophy of programming languages and into the logics that are used in CS to reason about them. The programming logics arising from CS are distinct from those originating in mathematics and logic because they must deal with partial functions.
Download article.

Principia Mathematica revolutionised our understanding of the nature of mathematics by showing that mathematics could be put on an objective footing. Today mathematicians still write mathematics in a largely informal language, but have a tacit consensus that the underlying content exists in formal representation like that of the Principia. We show how one can bridge the gap between these informal and formal representations.
Download article and slides.

Principia Mathematica inspired many developments in logic and the philosophy of mathematics, yet it also acquired a negative reputation in some quarters. Russell himself in his autobiography remarked that his intellect "never quite recovered from the strain" of writing it, while others were repelled by headline comments about their taking 400 pages to prove 1+1=2. However, thanks to the rise of the computer, we can now contemplate checking or even generating formal proofs of a size and intricacy that would have been quite impractical for anyone to do by hand, with practically perfect reliability. Formal proof in the Principia style can now be regarded not merely as an ideal but unrealistic theoretical possibility, but as a practical way of improving the reliability of proofs, either in mathematics or computer science and engineering. In my talk I will describe some of the successes of computer-checked formal proof and the challenges that remain.
Download slides.

We have formalized the type system implicit in the Principia Mathematica of Russell and Whitehead (it is nowhere actually presented in a completely formal manner, but the intention can be deduced) and developed a type-checking program for propositions and terms. In keeping with the approach taken in Principia, the types inferred from a term are the most general types possible. A curious feature, unusual in the context of type inference, is that reasoning about arithmetic inequalities' has to be implemented to handle orders. We have begun to develop a formalization of reasoning in the logic of the Principia and will discuss this if time permits.
Download article and slides.

In Russell's Ramified Type Theory RTT as presented in Principia Mathematica, two hierarchical concepts dominate: orders and types. In this talk we reflect on the lessons learned from orders and types and on the progress in the formalisation of mathematics since the work of Frege, Russell, Whitehead and others. In particular we reflect on how mathematicians and logicians still use types differently and how types and orders have developed since Russell to accommodate the formalisation of mathematics and logic.
Download article.

Despite initial appearances, there are actually very few theorems in Principia Mathematica. This is because of typical ambiguity: most of the strings of signs which look like theorems only become so once the ambiguities have been resolved. I shall discuss whether we should care about this.

This paper examines the no-class theory of Principia Mathematica. By drawing the scope distinction for class terms, it argues that the theory fails to preserve the logic of classes. And the paper presents a modification of the theory, the plural no-class theory, that resolves logical problem of PM's theory, and preserves the logic of classes. Then the paper argues that the plural no-class theory does not yield the view that there are no classes, but the view that classes can be identified as propositional functions (or properties) of a special kind, namely, the predicative ones.
Download article.