[Prev][Next][Index][Thread]
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.