[Prev][Next][Index][Thread]

Two papers on higher-order polymorphism and subtyping


Two new papers combining higher-order polymorphism and subtyping are
now available for anonymous FTP.  Beginning from a common foundation,
both use proof-theoretic techniques to obtain related -- but
independently derived -- decidability results, one [Steffen and
Pierce] for the pure system FomegaSub of higher-order bounded
quantification, the other [Compagnoni] for FomegaSub enriched with
intersection types, FomegaMeet.  Abstracts and FTP instructions
follow.

Enjoy,

        Adriana Compagnoni  (abc@dcs.ed.ac.uk)
        Benjamin Pierce     (bcp@dcs.ed.ac.uk)
        Martin Steffen      (mnsteffe@informatik.uni-erlangen.de)

------------------------------------------------------------------------

                 Subtyping in FomegaMeet is decidable

                        Adriana B. Compagnoni

Combining intersection types with higher-order subtyping yields a
typed model of object-oriented programming with multiple inheritance
[CompagnoniPierce93].  The target calculus, FomegaMeet, a natural
generalization of Girard's system Fomega with intersection types and
bounded polymorphism, is of independent interest.  We prove that
subtyping in FomegaMeet is decidable, which yields as a corollary the
decidability of subtyping in FomegaSub, its intersection free
fragment, because FomegaMeet subtyping system is a conservative
extension of that of FomegaSub.  Since in both cases subtyping is
closed under beta-meet-conversion or beta-conversion of types, which
is not the case for the calculus presented in [CastagnaPierce93],
solving the problem in the present setting is much more difficult.

Moreover, we establish basic structural properties of FomegaMeet and
we prove that the type assignment system is sound using a model based
on partial equivalence relations.


FTP instructions:

    ftp ftp.cs.kun.nl                   [or 131.174.33.1]
    login: anonymous
    password: <your mail address>
    cd pub/csi/CompMath/Types
    binary			        [don't forget this!]
    get FomegaMeet.dvi                  [or FomegaMeet.ps]

------------------------------------------------------------------------

                        Higher-Order Subtyping

                  Martin Steffen and Benjamin Pierce

System FomegaSub 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, eliminability of the "cut-rule" of transitivity
from the subtype relation, and the soundness, completeness, and
termination of algorithms for subtyping and typechecking.


FTP instructions:

    ftp ftp.dcs.ed.ac.uk                [or 129.215.160.5]
    login: anonymous
    password: <your mail address>
    cd pub/bcp
    binary			        [don't forget this!]
    get fomega.dvi.Z                    [or fomega.ps]

(Also available from ftp.uni-erlangen.de [131.188.1.43] from the
directory /pub/papers/immd7/sfbc2.)