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

paper on an extension of linear types




I would like to announce the following technical report
(available at http://www.yl.is.s.u-tokyo.ac.jp/~koba/pub/qlinear.ps.gz).
Comments are welcome.

	Quasi-Linear Types
	 Naoki Kobayashi

Abstract

Linear types (types of values that can be used just once) have been
drawing great attentions because they are useful for memory
management, in-place update of data structures, etc.: an obvious
advantage is that a value of a linear type can be immediately
deallocated after being used.  However, the linear types have not been
applied so widely in practice, probably because linear values (values
of linear types) in the traditional sense do not so often appear in
actual programs.  In order to increase the applicability of linear
types, we relax the condition of linearity by extending the types with
information on an evaluation order and simple dataflow
information. The extended type system, called a quasi-linear type
system, is formalized and its correctness is proved. We have
implemented a prototype type inference system for the core-ML that can
automatically find out which value is linear in the relaxed sense.
Promising results were obtained from preliminary experiments with the
prototype system.

-- 
Naoki Kobayashi
Department of Information Science
Faculty of Science
University of Tokyo
7-3-1 Hongo, Bunkyo-ku,
Tokyo 113, Japan
e-mail:koba@is.s.u-tokyo.ac.jp
http://www.yl.is.s.u-tokyo.ac.jp/~koba/home.html