Subtype Universes in a Flat Type Theory
Project: Research
- Bradley, Felix (PI)
Description
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.
| Status | Active |
|---|---|
| Effective start/end date | 19/04/22 → … |
ID: 45319525