[logic-ml] Talk by Kohei Suenaga, Thursday next week (2010.12.2)

[Ichiro Hasuo]

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.