Anti-Symmetry of Higher-Order Subtyping

10 years 3 months ago
Anti-Symmetry of Higher-Order Subtyping
This paper gives the first proof that the subtyping relation of a higherorder lambda calculus, Fω ≤, is anti-symmetric, establishing in the process that the subtyping relation is a partial order—reflexive, transitive, and anti-symmetric up to β-equality. While a subtyping relation is reflexive and transitive by definition, anti-symmetry is a derived property. 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: of particular importance is our extended rule for the well-formedness of types with head variables. The paper also gives a presentation of Fω ≤ without a relation for β-equality, apparently the first such, and shows its equivalence with the traditional presentation.
Adriana B. Compagnoni, Healfdene Goguen
Added 04 Aug 2010
Updated 04 Aug 2010
Type Conference
Year 1999
Where CSL
Authors Adriana B. Compagnoni, Healfdene Goguen
Comments (0)