Step-indexed semantic models of types were proposed as an alternative to the
purely syntactic proofs of type safety using subject-reduction. This thesis
a step-indexed model for the functional object calculus, and uses it to
prove the soundness of an expressive type system with object types, subtyping,
recursive and bounded quantified types.