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