Paper on bounded quantification with a Bottom type

The following paper is available electronically via:



        Benjamin Pierce


                  Bounded Quantification with Bottom

                          Benjamin C. Pierce
                          Indiana University

                      CSCI Technical Report #492

While numerous extensions of Cardelli and Wegner's calculus of
polymorphism and subtyping, Kernel Fun, have been studied during the
past decade, one quite simple one has received little attention: the
addition of a minimal type Bot, dual to the familiar maximal type

We develop basic meta-theory for this extension.  Although most of the
usual properties of Kernel Fun (existence of meets and joins,
decidability of subtyping and typing, subject reduction, etc.) also
hold for the extended system, the presence of Bot introduces some
surprising intricacies.  In particular, a type variable bounded by Bot
is actually a synonym for Bot; such "bottom variables" must be treated
specially at several points.