Abstract: System F omega sub is an extension with subtyping of Girard's higher-order polymorphic lambda-calculus. We develop the fundamental metatheory of this calculus: decidability of beta-conversion on well-kinded types, elimination of the ``cut-rule'' of transitivity from the subtype relation, and the soundness, completeness, and termination of algorithms for subtyping and typechecking.
Previous | Index | Next An error occured whilst processing this directive