\begin{abstract}
A general method of interpreting weak higher-type theories of
nonstandard arithmetic in their standard counterparts is presented.
In particular, this provides natural nonstandard conservative
extensions of primitive recursive arithmetic, elementary recursive
arithmetic, and polynomial-time computable arithmetic. A means
of formalizing basic real analysis in such theories is sketched.
\end{abstract}