[Prev][Next][Index][Thread]
Two papers on higher-order polymorphism and subtyping
-
To: types@uk.ac.gla.dcs
-
Subject: Two papers on higher-order polymorphism and subtyping
-
From: Benjamin Pierce <bcp@uk.ac.ed.dcs>
-
Date: Fri, 07 Jan 94 20:14:50 GMT
-
Approved: types@dcs.gla.ac.uk
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.)