Abstract

The logic BI of bunched implications mixes multiplicative and additive features using a tree-like notion of context, or bunch has its roots in relevant logic. We give a computational interpretation of BI's associated type system, the alpha-lambda-calculus, in terms of a notion of regions of aliasing. The programming model is that of a store broken into regions of pointers; pointers within the same region may be aliased, but pointers in different regions may not be. We describe an interpretation where the multiplicative implication A-*B corresponds to procedures that access disjoint regions from their arguments, and the additive A->B corresponds to procedures that access the same regions as their arguments. Generally, multiplicative conntectives control aliasing and extrusion, while the additives allow it. An explicit distinction is made between heap and stack allocation.