Typed-operational semantics for higher-order subtyping

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 <f>Fω&les;</f>, a variant of <f>F<:ω</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 <f>Fω&les;</f>, using logical relations to prove soundness. The typed-operational semantics provides a powerful and uniform technique to study metatheoretic properties of <f>Fω&les;</f>, 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. [Copyright &y& Elsevier]