Order-theoretic Differences Between Two Variants of Type Theory
by Evan Moran
2012
Two versions of computational type theory under active development around town are Nuprl 5 and a (still-unnamed) variant of it that arises from Howe's classical, set-theoretic semantics. This intermediate-level seminar will compare an aspect of their related but different subtyping orders.