4pm Tuesday 21st January 2003
Room 2511, JCMB, King's Buildings
Hofmann's LFPL is a functional language with constructs which can be interpreted as referring to heap locations. In this view, the language is suitable for expressing and verifying in-place update algorithms. Correctness of this semantics is achieved by a linear typing. We introduce a non-linear typing of first-order LFPL programs which is more permissive than the recent effect-based typing of Aspinall and Hofmann. The system efficiently infers separation assertions in the sense of Reynolds' Separation Logic as well as destruction and re-use effects for individual layers of recursive-type values. Thus it is suitable for expressing and analysing in-place update algorithms with complicated data aliasing.