Bounded operator abstraction is a language construct relevant to object-oriented programming languages and to ML2000, the successor to Standard ML. In this paper, we introduce ℱ≤ω, a variant of F<:ωwith this feature and with Cardelli and Wegner's kernel Fun rule for quantifiers. We define a typed operational semantics with subtyping and prove that it is equivalent with ℱ≤ω, using logical relations to prove soundness. The typed operational semantics provides a powerful and uniform technique to study metatheoretic properties of ℱ≤ω, such as Church-Rosser, subject reduction, the admissibility of structural rules, and the equivalence with the algorithmic presentation of the system that performs weak-head reductions. Furthermore, we can show decidability of subtyping using the typed operational semantics and its equivalence with the usual presentation. Hence, this paper demonstrates for the first time that logical relations can be used to show decidability of subtyping. © 2003 Elsevier Science (USA). All rights reserved.
Compagnoni, A., & Goguen, H. (2003). Typed operational semantics for higher-order subtyping. Information and Computation, 184(2), 242–297. https://doi.org/10.1016/S0890-5401(03)00062-2