Personal tools
You are here: Home Events Abstract Archives 2003 Functional In-place Update with Layered Datatype Sharing

Functional In-place Update with Layered Datatype Sharing

Michal Konecný LFCS 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.

Document Actions