Copenhagen Programming Language Seminar


On the correctness of region inference

Henning Niss
Department of Innovation, It University of Copenhagen

Thursday, April 10th, 15:15-16:00
IT-C, Glentevej 67, room 2.03


Region inference decorates a program with "region annotations" that makes memory-management actions explicit. The key properties that one wishes to establish about region inference is "memory safety" and "conditional correctness". Memory safety shows that an annotated program does not go wrong due to memory errors. Conditional correctness shows that, assuming that the region annotated program is memory safe, then its observable semantics is the same as that of the original unannotated program.

We give a brief survey of correctness results in the literature. Except for the seminal paper by Tofte and Talpin, previous work has focused on establishing memory safety. The correctness result by Tofte and Talpin also establishes conditional correctness, but in a complex co-inductive fashion. We present a small language with region annotations and show how to prove both memory safety and conditional correctness in a simple syntactic fashion.

Scientific host: Peter Sestoft. Administrative host: Camilla Jensen. All are welcome.
The Copenhagen Programming Language Seminar (COPLAS) is a collaboration between DIKU, IT-C and KVL.
To receive information about COPLAS talks by email, send a message to prog-lang-request@mail.it-c.dk with the word 'subscribe' as subject or in the body.

For more information about COPLAS, see http://www.coplas.org