2 papers
cs.LO2025
Internalizing Extensions in Lattices of Type Theories
Jonathan Chan
Many proof assistants allow the use of features and axioms that increase their expressive power. However, these extensions must be used with care, as some combinations are known to…
cs.PL2025
Bounded First-Class Universe Levels in Dependent Type Theory
Jonathan Chan, Stephanie Weirich
In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from…