Dear colleagues,

Next week on Thursday our guest Kohei Suenaga (U. Lisbon, ex. Tohoku U) is making a talk at RIMS, Kyoto University. No registration necessary. See you there!

Best regards, Ichiro Hasuo --- RIMS-CS website http://www.kurims.kyoto-u.ac.jp/~cs/

===== Speaker: Kohei Suenaga (Universidade de Lisboa, Portugal)

Title: Fractional Ownerships for Safe Memory Deallocation

Date: 11.00 - 12.00, Thu 2 Dec 2010

Place: Room 478, "Research Bldg. No. 2 (Sougou Kenkyu 2-Goukan)" http://www.kyoto-u.ac.jp/en/access/campus/main.htm (Next to our CS Lab) 総合研究2号館 478号室 (CS室のとなりです) http://www.kyoto-u.ac.jp/ja/access/campus/map6r_y.htm

Abstract:

We propose a type system for a programming language with memory allocation/deallocation primitives, which prevents memory-related errors such as double-frees and memory leaks. The main idea is to augment pointer types with fractional ownerships, which express both capabilities and obligations to access or deallocate memory cells. By assigning an ownership to each pointer type constructor (rather than to a variable), our type system can properly reason about list/tree- manipulating programs. Furthermore, thanks to the use of fractions as ownerships, the type system admits a polynomial-time type inference algorithm, which serves as an algorithm for automatic verification of lack of memory-related errors. A prototype verifier has been implemented and tested for C programs.

This is joint work with Naoki Kobayashi.