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

Higher-order polymorphism: corrected version


A few weeks ago, we announced a paper on the basic proof theory of
FOmegaSub, a higher-order extension of bounded quantification.
Giorgio Ghelli's recent observation that FSubTop fails to possess
minimal types revealed an error in one section of our paper, in which
we claimed that our extension *did* possess minimal types.  We have
corrected the error by replacing the top-rule for subtyping of bounded
quantifiers with Cardelli and Wegner's original Fun-rule.  Most of our
analysis goes through essentially unchanged (except the proof of
termination of subtyping, which required a new idea).

If you retrieved a copy of the erroneous version, we would appreciate
your discarding it and replacing it with the new one.  

Cheers,

        Benjamin Pierce
        Martin Steffen

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

                        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]

For WWW-literati:
   ftp://ftp.dcs.ed.ac.uk/pub/bcp/fomega.dvi.Z