Personal tools
You are here: Home Events Abstract Archives 2000 Antisymmetry of higher-order subtyping

Antisymmetry of higher-order subtyping

Adriana Compagnoni Stevens Institute of Technology 11am Friday 24 March 2000 Room 2511, JCMB, King's Buildings

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.

Document Actions