> Some programs in the Simply Typed Lambda Calculus [^1] have no type—i.e. diverging programs.
Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus
Nitpick, because those programs have no type they are not members of the Simply Typed Lambda Calculus but only of the underlying untyped calculus