We describe an encoding of major parts of domain theory and
fixed-point theory in the {\sc PVS} extension of the simply-typed
$\lambda$-calculus; these formalizations comprise the encoding of
mathematical structures like complete partial orders (domains), domain
constructions, the Knaster-Tarski fixed-point theorem for monotonic
functions, and variations of fixed-point induction.  Altogether, these
encodings form a conservative extension of the underlying {\sc Pvs}
logic.  A major problem of embedding mathematical theories like domain
theory lies in the fact that developing and working with those
theories usually generates myriads of applicability and
type-correctness conditions.  Our approach to exploiting the {\sc Pvs}
devices of {\em predicate subtypes} and {\em judgements} to establish
many applicability conditions {\em behind the scenes} leads to a
considerable reduction in the number of the conditions that actually
need to be proved.  We illustrate the applicability of our encodings
by means of simple examples including a mechanized fixed-point
induction proof in the context of relating different semantics of
imperative programming constructs.