Paper on bounded quantification with a Bottom type

• To: types@cs.indiana.edu
• Subject: Paper on bounded quantification with a Bottom type
• From: Benjamin Pierce <pierce@cs.indiana.edu>
• Date: Wed, 12 Nov 1997 17:47:39 -0500
• Delivery-Date: Wed, 12 Nov 1997 17:47:42 -0500
• Reply-to: pierce@cs.indiana.edu

The following paper is available electronically via:

        http://www.cs.indiana.edu/hyplan/papers/bqb.ps.gz

Enjoy,

        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
Top.

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.

• Prev: Two papers on "local type inference"
• Next: LICS'98: 2nd Call for Papers (text & LaTeX)
• Index(es):
  • Main
  • Thread