An Order-Theoretic Analysis of Universe Polymorphism
- 講者侯昆邦 教授 (美國明尼蘇達大學)
邀請人：穆信成 - 時間2023-07-19 (Wed.) 10:00 – 12:00
- 地點資訊所新館107演講廳
摘要
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).