Name
Abstract | ||
|---|---|---|
This paper shows that the subtyping relation of a higher-order lambda calculus, F≤ω, 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 up to β-equality. While a subtyping relation is reflexive and transitive by definition, antisymmetry is a derived property. The result, which may seem obvious to the nonexpert, 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. |
Year | DOI | Venue |
|---|---|---|
1999 | 10.1007/3-540-48168-0_30 | CSL |
Keywords | Field | DocType |
extended rule,open problem,subtyping relation,higher-order lambda calculus,traditional presentation,operational semantics,particular importance,head variable,powerful new technology,partial order,higher-order subtyping,higher order,lambda calculus | Covariance and contravariance,Discrete mathematics,Lambda calculus,Operational semantics,Open problem,Computer science,Pure mathematics,Type theory,Equivalence (measure theory),Subtyping,Calculus,Transitive relation | Conference |
Volume | ISSN | ISBN |
1683 | 0302-9743 | 3-540-66536-6 |
Citations | PageRank | References |
6 | 0.57 | 19 |
Authors | ||
2 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adriana B. Compagnoni | 1 | 62 | 7.16 |
| Healfdene Goguen | 2 | 75 | 8.24 |