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

two preliminary papers by anon ftp





Preliminary versions of two papers are available by anonymous ftp.
The titles and abstracts are given below. The files are

   ftp/pub/jcm/objects-paper.dvi
   ftp/pub/jcm/weak-poly.dvi

on theory.stanford.edu. Any comments, criticism, or corrections to
these papers will be appreciated.

John Mitchell


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


            A lambda calculus of objects and method specialization


     John C. Mitchell           Furio Honsell               Kathleen Fisher
   Computer Science Dept.  Dipartimento di Informatica   Computer Science Dept.
   Stanford University        Universit\'{a} di Udine      Stanford University 
   jcm@cs.stanford.edu       honsell@uduniv.cineca.it    kfisher@cs.stanford.edu


                           Abstract 

         This paper presents an untyped lambda calculus, extended with
      object primitives that reflect the capabilities of so-called
      delegation-based object-oriented languages.
      A type inference system allows static detection of errors,
      preventing {\it message not understood,}
      while at the same time allowing the type of an inherited
         method to be specialized to the type of the inheriting object.
         Type soundness, in the form of a ``subject-reduction'' theorem,
         is proved and examples illustrating the expressiveness
         of the pure calculus are presented.


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


          Standard ML weak polymorphism and imperative constructs

               My Hoang   John Mitchell  Ramesh Viswanathan
                     Department of Computer Science 
                Stanford University, Stanford, CA 94305
              {hoang, mitchell, vramesh}@cs.stanford.edu

                           Abstract 

Standard ML uses ``weak type variables'' to restrict  the polymorphic
use of functions that may allocate reference cells, manipulate
continuations, or use exceptions. However, the type system used in the
Standard ML of New Jersey (SML-NJ) compiler has not been presented in
a form other than source code and has not been proved correct.
We present a set of typing rules, using only weak type variables
of a slightly more general nature than the compiler,
that appears to subsume the implemented algorithm.
One insight is that the indexed type of a free variable
is used in two ways, once in describing the applicative
behavior of the variable itself, and once in describing
the larger term containing the variable. This allows
us to formulate an application rule that is more general
than SML-NJ for applications of polymorphic functions
to imperative arguments. The soundness of the type system
is proved for imperative code using operational semantics,
by a technique that involves equivalence classes of related type
variables.