Abstract: Recent Results in Type Theory and their Applications in MetaPRL and Nuprl

Bob Constable

We examine Kopylov's dependent intersection type and its use in defining dependent records which are a basis for class theory. We also examine Nogin's new axioms for quotient types and their use in defining collections.

The talk will briefly mention applications of these ideas to validating distributed system components, and it will illustrate the Common Mathematics Library used by MetaPRL, Nuprl, JProver and other systems, comparing it to Automath's tree of knowledge.