Recent research topic of Naoki Kobayashi's group:

Quasi-Linear Types

• What is a quasi-linear type system?

  Linear type systems distinguish between the type of a value that can be used just once and the type of a value that can be used many times. This distinction can be used for improvement of memory management and in-place update of data structures: if a heap value is statically known to be used just once, it can be automatically deallocated when it is accessed. A quasi-linear type system is an extension of linear type systems. Because usual linear type systems count the access to a value strictly, they cannot be used for deallocating values that are used more than once. For example, it is trivial that x can be deallocated after x+y is evaluated in the following program

  let val x = 1.0 in let val y = x+1.0 in x+y end end

  but linear type systems cannot do that because x is used twice. We overcame this kind of problem by extending a linear type system with information on the evaluation order and dataflow. See the paper below for more information.

• Paper (see also Kobayashi's publication page for related papers)

  • Naoki Kobayashi, Quasi-Linear Types, technical report TR98-02, Department of Information Science, University of Tokyo (Summary will be presented at ACM POPL'99).

• Prototype analyzer

  We have implemented a prototype analyzer that takes a core-ML (Standard ML without modules) expression as an input, performs type reconstruction based on the quasi-linear type system, and outputs a program annotated with information on which value is (quasi-)linear. The system uses the ML kit as a front end. It is not yet ready for wide distribution, but if you want to test it now, the source code (written in SML-NJ93) and executable file (Ver.0.21) for Sun SPARCstations (and sample test programs) are temporalily available from here.