Abstract

This talk is about joint research with Healfdene Goguen. This work shows that the subtyping relation of a higher-order lambda calculus, (F-omega-sub with bounded operator abstraction), is anti-symmetric. It exhibits the first such proof, establishing in the process that the subtyping relation is a partial order---reflexive, transitive and anti-symmetric. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. This property has been conjectured by many researchers in the community but never proved. The result, which may seem obvious to the non-expert, is technically challenging, and had been an open problem for almost a decade. In this context, typed operational semantics for subtyping offers a powerful new technology to solve the problem.