hide
Free keywords:
-
Abstract:
System Fsub, the second-order polymorphic typed lambda-calculus with
subtyping [Cardelli-Wegner, 85], [Bruce-Longo, 90], [Curien-Ghelli, 92],
appeared to be undecidable because of the undecidability of its
subtyping component [Pierce, 92]. The discovery of decidable
extensions of the Fsub-subtyping relation [Vorobyov 94] put forward
a challenging problem of incorporating these extensions into an
Fsub-like typing in a decidable and coherent manner. In this paper
we describe a family of systems combining the standard Fsub-typing
rules with converging hierarchies of decidable extensions of the
Fsub-subtyping and give decidable criteria for successful proof
normalization and subject reduction.
