Strong Update, Disposal, and Encapsulation in Bunched Typing

Josh Berdine, Peter W. O'Hearn

Electronic Notes in Theoretical Computer Science | , Vol 158: pp. 81-98

We present a bunched intermediate language for strong (type-changing) update and disposal of first-order references. In contrast to other substructural type systems, the additive constructs of bunched types allow the encapsulation of state that is shared by a collection of procedures.