Another Type System for In-Place Update

David Aspinall, Martin Hofmann

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Linear typing schemes guarantee single-threadedness and so the soundness of in-place update with respect to a functional semantics. But linear schemes are restrictive in practice, and more restrictive than necessary to guarantee soundness of in-place update. This has prompted research into static analysis and more sophisticated typing disciplines, to determine when in-place update may be safely used, or to combine linear and non-linear schemes. Here we contribute to this line of research by defining a new typing scheme which better approximates the semantic property of soundness of in-place update for a functional semantics. Our typing scheme includes two kinds of products ( ⊗and x), which allows data structures with or without sharing to be defined.We begin from the observation that some data is used only in a “read-only” context after which it may be safely re-used before being destroyed. Formalizing the inplace update interpretation and giving a machine model semantics allows us to refine this observation.We define three usage aspects apparent from the semantics, which are used to annotate function argument types. The aspects are (1) used destructively, (2) used read-only but shared with result, and (3) used read-only and not shared.
Original languageEnglish
Title of host publicationProgramming Languages and Systems
Subtitle of host publication11th European Symposium on Programming, ESOP 2002 Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2002 Grenoble, France, April 8–12, 2002 Proceedings
EditorsDaniel Le Métayer
PublisherSpringer Berlin Heidelberg
Pages36-52
Number of pages17
Volume2305
ISBN (Electronic)978-3-540-45927-9
ISBN (Print)978-3-540-43363-7
DOIs
Publication statusPublished - 2002

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin Heidelberg
Volume2305

Fingerprint

Dive into the research topics of 'Another Type System for In-Place Update'. Together they form a unique fingerprint.

Cite this