An Order-Theoretic Analysis of Universe Polymorphism
- LecturerProf. Kuen-Bang Hou (Favonia) (University of Minnesota)
Host: Shin-Cheng Mu - Time2023-07-19 (Wed.) 10:00 ~ 12:00
- LocationAuditorium107 at IIS new Building
Abstract
Universe polymorphism is a common feature in proof assistants to improve their usability. We present a novel formulation of universe polymorphism in terms of monads, and a novel algebraic structure, displacement algebras, on top of which one can implement a generalized form of McBride’s “crude but effective stratification” scheme for universe polymorphism. We then argue that this generalized form of McBride’s scheme is the most general. Many of our technical results have been mechanized in Agda (https://github.com/RedPRL/agda-mugen), and we have an OCaml library (https://github.com/RedPRL/mugen) for developing proof assistants with universe polymorphism. This joint work with Carlo Angiuli and my pre-doc Reed Mullanix has been published at POPL 2023 (https://doi.org/10.1145/3571250).