3 citations · 5 across the 4 of their papers we have counts for
Showing cs.PLShow all
3 papers · 1 filter
cs.PL2025★ 2 cited
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…
cs.PL2023
Stratified Type Theory
Jonathan Chan, Stephanie Weirich
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent func…
cs.PL2019★ 3 cited
Is Sized Typing for Coq Practical?
Jonathan Chan, Yufeng Li, William J. Bowman
Contemporary proof assistants such as Coq require that recursive functions be terminating and corecursive functions be productive to maintain logical consistency of their type theo…