Subtype Universes in a Flat Type Theory

Project: Research


Subtype universes were proposed as a solution to undecidability of type checking in previous implementations of bounded quantification. This project aims to construct a "flat" type theory without universes and look at the structure developed when adding subtype universes, with the goal of looking at the consistency and decidability of such.
Effective start/end date19/04/22 → …

ID: 45319525