The stratification function has recently been refined in two ways. Where embedded theorem names appear, they are checked for stratification internally but their type relative to the term to which they are attached is not checked. This is safe, since embedded theorems have no effect on term value. In addition, a predeclared infix : is provided which serves to generate type labels: the term t : x is the result of applying a retraction to x, determined by t, whose range is a ``strongly Cantorian set'' (a technical notion in set theories related to New Foundations). This has the effect of allowing the term to be freely raised and lowered in type. The effect of this on stratification is that one may freely raise and lower the types assigned to x and its subterms for purposes of stratifying the term in which it occurs; the type label should contain no type information (any variables in t must be restricted to strongly Cantorian sets). The only way in which types in x may influence stratification is that the difference between the types of two variables occurring in x may be fixed, and this will have to agree with the stratification of the context. This is motivated by the theoretical claim which we have made (in our paper in Modern Logic, vol. 4, no. 1) that ``strongly Cantorian set'' corresponds to ``data type'' in a model of computing based on this kind of set theory.
A further refinement along the same lines is that functions and operators whose input or output is restricted to a ``type'' (strongly Cantorian set) (this must be witnessed by a theorem) can be declared as ``scin'' (for strongly Cantorian input) or ``scout'' (for strongly Cantorian output). Stratification restrictions are relaxed accordingly, without any need for explicit type labels. For example, the equality infix = or a universal quantifier function forall can be declared ``scout'', since their output is boolean, and so the stratification function of the prover can exploit the fact that types of boolean-valued expressions can be freely raised and lowered in order to permit more complex abstractions. This feature should have the effect of minimizing the use of explicit type labels. Note that any use of operators declared ``scin'' or ``scout'' in abstraction terms has the effect of introducing dependencies on the witnessing theorems for those operators.
Examples of permissible types are booleans (or any finite set) and natural numbers. Cartesian products and function spaces built from strongly Cantorian sets are strongly Cantorian. Recursive and polymorphic type constructions will also work. The system of absolute types which can be built under Mark2 is thus as strong as that usually used in computer science.