How exactly is this notion of “semantic types” formalized? Is it something like NuPRL, where the base language's type system isn't sufficiently precise to rule

How exactly is this notion of “semantic types” formalized? Is it something like NuPRL, where the base language's type system isn't sufficiently precise to rule out all misbehaviors, and on top of that a more precise type system is added, whose typing rules might be defined in terms of the base language's evaluation/execution rules?