Strong Update, Disposal, and Encapsulation in Bunched Typing

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. Key words: bunched typing, separation logic, strong update, disposal, encapsulation, continuation-passing style

• Type: Journal
• Year: 2006
• Where: ENTCS
• Authors: Josh Berdine, Peter W. O'Hearn
• Keywords: ENTCS 2006, First-order References, Intermediate Language, Substructural Type Systems