This paper introduces a typed $\lambda$-calculus called
\lambdaPower, an improved formulation of a predicative fragment of
Cardelli's \emph{power type} system. Power types integrate
subtyping into the typing judgement, allowing bounded abstraction
and bounded quantification over both types and terms. This gives a
powerful and concise system of dependent types, but leads to
difficulty in the meta-theory and semantics which has impeded the
application of power types so far.
%
Basic properties of \lambdaPower are proved here, and it is given a
model definition using a form of applicative structures. A
particular novelty is the auxiliary system for \terminology{rough
typing}, which assigns simple types to terms in \lambdaPower.
These ``rough'' types are used to prove strong normalization of the
calculus and to structure models, allowing a novel form of
containment semantics without a universal domain.
