Fully Abstract Logical Bisimilarity for a Polymorphic Object Calculus

We characterise type structurally the termination observational congruence of Abadi and Cardellipsilas S_forall calculus. Pittspsila operational reasoning approach for polymorphic lambda calculi is enhanced with subtyping and primitive covariant object types. Labelling each object with a bound ordinal of terminating method invocations and regarding omega-bounded as unlabelled reduction we achieve a crucial object unwinding lemma. Value and term bisimilarities are suitably defined with novel type structural operators and (type-, relation- and value-environment) bindings. We prove term bisimilarity complete and sound with respect to observational congruence, postulated as the largest, substitutive, compatible, (termination) adequate and (type) subsumptive, well typed term relation.