BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TN-95-18
       ENTRY:: March 13, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Effective models of polymorphism, subtyping and recursion
        TYPE:: Technical Note
      AUTHOR:: Mitchell, John
      AUTHOR:: Viswanathan, Ramesh
        DATE:: March 1995
       PAGES:: 12
    ABSTRACT:: We develop a class of models of polymorphism, subtyping and
               recursion based on a combination of traditional recursion
               theory and simple domain theory. A significant property of
               our primary model is that types are coded by natural numbers
               using any index of their supremum operator. This leads to a
               distinctive view of polymorphic functions that has many of
               the usual parametricity properties. It also gives a
               distinctive but entirely coherent interpretation of
               subtyping. An alternate construction points out some
               peculiarities of computability theory based on natural number
               codings. Specifically, the polymorphic fixed point is
               computable by a single algorithm at all types when we
               construct the model over untyped call-by-value lambda terms,
               but not when we use Godel numbers for computable functions.
               This is consistent with trends away from natural numbers in
               the field of abstract recursion theory.
       NOTES:: [Adminitrivia V1/Prg/19950313]
         END:: STAN//CS-TN-95-18