Recording and Slides

Time and Location

  • Date: Wednesday, December 6
  • Time: 11:15 AM-12:15 PM
  • Location: Luddy Hall 1104 (BLIF-1104)

Abstract

Dependent type theory expresses type dependency and quantification in terms of a hierarchy of type universes whose elements are other types. In this talk, I will motivate universe hierarchies by discussing how they resolve paradoxes in naive set theory. Next, I will discuss a few mechanisms for universe polymorphism implemented in proof assistants to avoid code duplication.

Finally, I will talk about joint work with Favonia and Reed Mullanix (“An Order-Theoretic Analysis of Universe Polymorphism”, POPL 2023) in which we formulate general notions of universe hierarchies and universe polymorphism, give some examples of exotic but consistent universe hierarchies, and prove that any universe-polymorphic type theory can be presented via McBride’s “crude but effective stratification.”