Seminars will be held in the Lecture Theatre 1 - William Gates Building, Computer Laboratory at 4.15pm

	See also: Security seminars Logic and Semantics seminars Additional meetings weekly timetable for other meetings

Correctness of Data Representations Involving Heap Data Structures

Uday Reddy

University of Birmingham

A major aim of giving semantics to imperative and object-oriented programming languages in recent years has been to support the information hiding that goes on in such languages, in particular, relational reasoning principles for showing the correctness of data representations (also referred to as "data refinement"). The situation for programs with local variables is by now well-understood. But, similar semantics for programs that deal with heap data structures and pointers has proved elusive. In this talk, we report on a first semantic model for languages with heap data structures that validates data refinement. The model is built using a general framework for information hiding based on relational parametricity. The novelty is in finding appropriate relational correspondences that account for information leakage or "extrusion" that becomes possible with pointer data.