非表示:
キーワード:
-
要旨:
Step-indexed semantic models of types were proposed as an alternative to the
purely syntactic proofs of type safety using subject-reduction. This thesis
introduces
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.
