Lambda the Ultimate

An oldie (2000), but in my current (ignorant, admittedly) mind a goodie, from Igarashi & Kobayashi. I just wish the research hadn't apparently immediately died off? Garbage Collection Based on a Linear Type System. Or, chocolate + peanut butter.

We propose a type-directed garbage collection (GC) scheme for a programming language with static memory management based on a linear type system. Linear type systems, which can guarantee certain values (called linear values) to be used only once during program execution, are useful for memory management: memory space for linear values can be reclaimed immediately after they are used. However, conventional pointer-tracing GC does not work under such a memory management scheme: as linear values are used, dangling pointers to the memory space for them will be yielded.

This problem is solved by exploiting static type information during garbage collection in a way similar to tag-free GC. Type information in our linear type system represents not only the shapes of heap objects but also how many times the heap objects are accessed in the rest of computation. Using such type information at GC-time, our GC can avoid tracing dangling pointers; in addition, our GC can reclaim even reachable garbage. We formalize such a GC algorithm and prove its correctness.

It looks like I might be in Tokyo over the winter holiday / new year. Long ago I attended the long defunct Starling meetup. Wondering if other LtUers will be around this 2015-16? (No, I don't speak Japanese.)

In general, it might be nice to let people know if/when we travel in case we want to take turns buying rounds of beers somewhere?