Skip to main content
PRL Project

Order-theoretic Differences Between Two Variants of Type Theory

by Evan Moran

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.