A transfinite type theory with type variables. - Andrews, P.B