Papers by anon ftp

Two papers are available by anonymous ftp from 
  machine: theory.stanford.edu
directory: pub/jcm
    files: weak-poly.dvi, objects-lic93.dvi


        Standard ML-NJ 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

Standard ML of New Jersey (SML-NJ) 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 SML-NJ
compiler has not been presented in a form other than source code and has not
been proved correct.  We present a type system, in the form of typing rules and
an equivalent algorithm, that appears to subsume the implemented algorithm.
Both use type variables of only a slightly more general nature than the
compiler.  One insight in the analysis 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.  Taking this into account, we 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. 


           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     Universita di Udine          Stanford University
jcm@cs.stanford.edu     honsell@uduniv.cineca.it     kfisher@cs.stanford.edu

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, such as
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.