2 papers
cs.PL2026
Contravariant Universe Subtyping, Formalized, Mechanized
Shengyi Jiang, Jason Z. S. Hu
In a type theory with a cumulative universe hierarchy, \emph{subtyping} is often incorporated to lift lower universe levels to higher ones. In practice, kernels of proof assistants…
cs.PL2026
Bidirectional Typing with Freezing, Skeletons, and Ghosts
Wenhao Tang, Shengyi Jiang, Aghilas Y. Boussaa +2
Bidirectional typing makes use of local information flow between functions and arguments. Conventional bidirectional typing only supports unidirectional information flow, typically…